Theorem catcocl 17668

Description: Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
catcocl.b	⊢ 𝐵 = (Base‘𝐶)
catcocl.h	⊢ 𝐻 = (Hom ‘𝐶)
catcocl.o	⊢ · = (comp‘𝐶)
catcocl.c	⊢ (𝜑 → 𝐶 ∈ Cat)
catcocl.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
catcocl.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
catcocl.z	⊢ (𝜑 → 𝑍 ∈ 𝐵)
catcocl.f	⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))
catcocl.g	⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))

Assertion

Ref	Expression
catcocl	⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))

Proof of Theorem catcocl

Dummy variables 𝑓 𝑔 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		catcocl.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ Cat)
2		catcocl.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐶)
3		catcocl.h	. . . . 5 ⊢ 𝐻 = (Hom ‘𝐶)
4		catcocl.o	. . . . 5 ⊢ · = (comp‘𝐶)
5	2, 3, 4	iscat 17655	. . . 4 ⊢ (𝐶 ∈ Cat → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))))))
6	5	ibi 266	. . 3 ⊢ (𝐶 ∈ Cat → ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))))
7		simpl 481	. . . . . . 7 ⊢ (((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
8	7	2ralimi 3112	. . . . . 6 ⊢ (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) → ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
9	8	2ralimi 3112	. . . . 5 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
10	9	adantl 480	. . . 4 ⊢ ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
11	10	ralimi 3072	. . 3 ⊢ (∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
12	1, 6, 11	3syl 18	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
13		catcocl.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
14		catcocl.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
15	14	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑌 ∈ 𝐵)
16		catcocl.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
17	16	ad2antrr 724	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑍 ∈ 𝐵)
18		catcocl.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))
19	18	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑋𝐻𝑌))
20		simpllr 774	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑥 = 𝑋)
21		simplr 767	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
22	20, 21	oveq12d 7437	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌))
23	19, 22	eleqtrrd 2828	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑥𝐻𝑦))
24		catcocl.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))
25	24	ad3antrrr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑌𝐻𝑍))
26		simpr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍)
27	21, 26	oveq12d 7437	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑦𝐻𝑧) = (𝑌𝐻𝑍))
28	25, 27	eleqtrrd 2828	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑦𝐻𝑧))
29	28	adantr 479	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝐺 ∈ (𝑦𝐻𝑧))
30		simp-5r 784	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑥 = 𝑋)
31		simp-4r 782	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑦 = 𝑌)
32	30, 31	opeq12d 4883	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩)
33		simpllr 774	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑧 = 𝑍)
34	32, 33	oveq12d 7437	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (⟨𝑥, 𝑦⟩ · 𝑧) = (⟨𝑋, 𝑌⟩ · 𝑍))
35		simpr 483	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
36		simplr 767	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
37	34, 35, 36	oveq123d 7440	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
38	30, 33	oveq12d 7437	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑥𝐻𝑧) = (𝑋𝐻𝑍))
39	37, 38	eleq12d 2819	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
40	29, 39	rspcdv 3598	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
41	23, 40	rspcimdv 3596	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
42	17, 41	rspcimdv 3596	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
43	15, 42	rspcimdv 3596	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
44	13, 43	rspcimdv 3596	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
45	12, 44	mpd 15	1 ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3050  ∃wrex 3059  ⟨cop 4636  ‘cfv 6549  (class class class)co 7419  Basecbs 17183  Hom chom 17247  compcco 17248  Catccat 17647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-cat 17651

This theorem is referenced by:  catcone0  17670  oppccatid  17704  ismon2  17720  isepi2  17727  sectco  17742  monsect  17769  catsubcat  17828  issubc3  17838  fullsubc  17839  idfucl  17870  cofucl  17877  fthsect  17917  fthmon  17919  fuccocl  17959  invfuc  17969  2initoinv  18002  initoeu2lem0  18005  initoeu2lem1  18006  initoeu2  18008  2termoinv  18009  coahom  18062  catcisolem  18102  xpccatid  18182  1stfcl  18191  2ndfcl  18192  prfcl  18197  evlfcllem  18216  evlfcl  18217  curf1cl  18223  curfcl  18227  hofcllem  18253  hofcl  18254  yon12  18260  hofpropd  18262  yonedalem4c  18272  srhmsubc  20625  bj-endmnd  36928  srhmsubcALTV  47573  endmndlem  48207  functhinclem4  48236  thincsect  48249

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »