Theorem catcocl 17626

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 17613	. . . 4 ⊢ (𝐶 ∈ Cat → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))))))
6	5	ibi 267	. . 3 ⊢ (𝐶 ∈ Cat → ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))))
7		simpl 482	. . . . . . 7 ⊢ (((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
8	7	2ralimi 3103	. . . . . 6 ⊢ (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) → ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
9	8	2ralimi 3103	. . . . 5 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
10	9	adantl 481	. . . 4 ⊢ ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
11	10	ralimi 3066	. . 3 ⊢ (∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
12	1, 6, 11	3syl 18	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
13		catcocl.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
14		catcocl.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
15	14	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑌 ∈ 𝐵)
16		catcocl.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
17	16	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑍 ∈ 𝐵)
18		catcocl.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))
19	18	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑋𝐻𝑌))
20		simpllr 775	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑥 = 𝑋)
21		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
22	20, 21	oveq12d 7387	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌))
23	19, 22	eleqtrrd 2831	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑥𝐻𝑦))
24		catcocl.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))
25	24	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑌𝐻𝑍))
26		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍)
27	21, 26	oveq12d 7387	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑦𝐻𝑧) = (𝑌𝐻𝑍))
28	25, 27	eleqtrrd 2831	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑦𝐻𝑧))
29	28	adantr 480	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝐺 ∈ (𝑦𝐻𝑧))
30		simp-5r 785	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑥 = 𝑋)
31		simp-4r 783	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑦 = 𝑌)
32	30, 31	opeq12d 4841	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩)
33		simpllr 775	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑧 = 𝑍)
34	32, 33	oveq12d 7387	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (⟨𝑥, 𝑦⟩ · 𝑧) = (⟨𝑋, 𝑌⟩ · 𝑍))
35		simpr 484	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
36		simplr 768	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
37	34, 35, 36	oveq123d 7390	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
38	30, 33	oveq12d 7387	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑥𝐻𝑧) = (𝑋𝐻𝑍))
39	37, 38	eleq12d 2822	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
40	29, 39	rspcdv 3577	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
41	23, 40	rspcimdv 3575	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
42	17, 41	rspcimdv 3575	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
43	15, 42	rspcimdv 3575	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
44	13, 43	rspcimdv 3575	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
45	12, 44	mpd 15	1 ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  ⟨cop 4591  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  Hom chom 17207  compcco 17208  Catccat 17605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-cat 17609

This theorem is referenced by:  catcone0  17628  oppccatid  17660  ismon2  17676  isepi2  17683  sectco  17698  monsect  17725  catsubcat  17781  issubc3  17791  fullsubc  17792  idfucl  17823  cofucl  17830  fthsect  17869  fthmon  17871  fuccocl  17909  invfuc  17919  2initoinv  17952  initoeu2lem0  17955  initoeu2lem1  17956  initoeu2  17958  2termoinv  17959  coahom  18012  catcisolem  18052  xpccatid  18129  1stfcl  18138  2ndfcl  18139  prfcl  18144  evlfcllem  18162  evlfcl  18163  curf1cl  18169  curfcl  18173  hofcllem  18199  hofcl  18200  yon12  18206  hofpropd  18208  yonedalem4c  18218  srhmsubc  20600  bj-endmnd  37299  srhmsubcALTV  48306  endmndlem  48997  upeu2lem  49010  imaf1co  49137  fthcomf  49139  upciclem3  49150  upeu2  49154  uptrlem1  49192  swapfcoa  49263  fuco22natlem  49327  fucocolem1  49335  oppcthinco  49421  functhinclem4  49429  thincsect  49449