catcisolem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > catcisolem		Structured version Visualization version GIF version

Theorem catcisolem 18017

Description: Lemma for catciso 18018. (Contributed by Mario Carneiro, 29-Jan-2017.)

**Hypotheses**
Ref	Expression
catciso.c	⊢ 𝐶 = (CatCat‘𝑈)
catciso.b	⊢ 𝐵 = (Base‘𝐶)
catciso.r	⊢ 𝑅 = (Base‘𝑋)
catciso.s	⊢ 𝑆 = (Base‘𝑌)
catciso.u	⊢ (𝜑 → 𝑈 ∈ 𝑉)
catciso.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
catciso.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
catcisolem.i	⊢ 𝐼 = (Inv‘𝐶)
catcisolem.g	⊢ 𝐻 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)))
catcisolem.1	⊢ (𝜑 → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
catcisolem.2	⊢ (𝜑 → 𝐹:𝑅–1-1-onto→𝑆)

**Assertion**
Ref	Expression
catcisolem	⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨^◡𝐹, 𝐻⟩)

Distinct variable groups: 𝑥,𝑦,𝐶 𝑥,𝐹,𝑦 𝑥,𝐺,𝑦 𝜑,𝑥,𝑦 𝑥,𝐼,𝑦 𝑥,𝑅,𝑦 𝑥,𝑆,𝑦 𝑥,𝑋,𝑦 𝑥,𝑌,𝑦 Allowed substitution hints: 𝐵(𝑥,𝑦) 𝑈(𝑥,𝑦) 𝐻(𝑥,𝑦) 𝑉(𝑥,𝑦)

Proof of Theorem catcisolem Dummy variables 𝑓 𝑔 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		catcisolem.2	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑅–1-1-onto→𝑆)
2		f1ococnv1 6792	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
4	1	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅–1-1-onto→𝑆)
5		f1of 6763	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → 𝐹:𝑅⟶𝑆)
6	4, 5	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅⟶𝑆)
7		simp2 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑢 ∈ 𝑅)
8	6, 7	ffvelcdmd 7018	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑢) ∈ 𝑆)
9		simp3 1138	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑣 ∈ 𝑅)
10	6, 9	ffvelcdmd 7018	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑣) ∈ 𝑆)
11		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑥 = (𝐹‘𝑢))
12	11	fveq2d 6826	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑥) = (^◡𝐹‘(𝐹‘𝑢)))
13		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑦 = (𝐹‘𝑣))
14	13	fveq2d 6826	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑦) = (^◡𝐹‘(𝐹‘𝑣)))
15	12, 14	oveq12d 7364	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
16	15	cnveqd 5814	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
17		catcisolem.g	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)))
18		ovex 7379	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
19	18	cnvex 7855	. . . . . . . . . . . . 13 ⊢ ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
20	16, 17, 19	ovmpoa 7501	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑢) ∈ 𝑆 ∧ (𝐹‘𝑣) ∈ 𝑆) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
21	8, 10, 20	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
22		f1ocnvfv1 7210	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
23	4, 7, 22	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
24		f1ocnvfv1 7210	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
25	4, 9, 24	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
26	23, 25	oveq12d 7364	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = (𝑢𝐺𝑣))
27	26	cnveqd 5814	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = ^◡(𝑢𝐺𝑣))
28	21, 27	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡(𝑢𝐺𝑣))
29	28	coeq1d 5800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)))
30		catciso.r	. . . . . . . . . . 11 ⊢ 𝑅 = (Base‘𝑋)
31		eqid 2731	. . . . . . . . . . 11 ⊢ (Hom ‘𝑋) = (Hom ‘𝑋)
32		eqid 2731	. . . . . . . . . . 11 ⊢ (Hom ‘𝑌) = (Hom ‘𝑌)
33		catcisolem.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
34	33	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
35	30, 31, 32, 34, 7, 9	ffthf1o 17828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)))
36		f1ococnv1 6792	. . . . . . . . . 10 ⊢ ((𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
37	35, 36	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
38	29, 37	eqtrd 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
39	38	mpoeq3dva 7423	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣))))
40		fveq2 6822	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩))
41		df-ov 7349	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑋)𝑣) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩)
42	40, 41	eqtr4di 2784	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = (𝑢(Hom ‘𝑋)𝑣))
43	42	reseq2d 5927	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑋)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
44	43	mpompt 7460	. . . . . . 7 ⊢ (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
45	39, 44	eqtr4di 2784	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))))
46	3, 45	opeq12d 4830	. . . . 5 ⊢ (𝜑 → ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩ = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
47		inss1 4184	. . . . . . . . 9 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Full 𝑌)
48		fullfunc 17815	. . . . . . . . 9 ⊢ (𝑋 Full 𝑌) ⊆ (𝑋 Func 𝑌)
49	47, 48	sstri 3939	. . . . . . . 8 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Func 𝑌)
50	49	ssbri 5134	. . . . . . 7 ⊢ (𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺 → 𝐹(𝑋 Func 𝑌)𝐺)
51	33, 50	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹(𝑋 Func 𝑌)𝐺)
52		catciso.s	. . . . . . 7 ⊢ 𝑆 = (Base‘𝑌)
53		eqid 2731	. . . . . . 7 ⊢ (Id‘𝑌) = (Id‘𝑌)
54		eqid 2731	. . . . . . 7 ⊢ (Id‘𝑋) = (Id‘𝑋)
55		eqid 2731	. . . . . . 7 ⊢ (comp‘𝑌) = (comp‘𝑌)
56		eqid 2731	. . . . . . 7 ⊢ (comp‘𝑋) = (comp‘𝑋)
57		catciso.c	. . . . . . . . . 10 ⊢ 𝐶 = (CatCat‘𝑈)
58		catciso.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
59		catciso.u	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
60	57, 58, 59	catcbas 18008	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
61		inss2 4185	. . . . . . . . 9 ⊢ (𝑈 ∩ Cat) ⊆ Cat
62	60, 61	eqsstrdi 3974	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ Cat)
63		catciso.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
64	62, 63	sseldd 3930	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ Cat)
65		catciso.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
66	62, 65	sseldd 3930	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Cat)
67		f1ocnv 6775	. . . . . . . 8 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → ^◡𝐹:𝑆–1-1-onto→𝑅)
68		f1of 6763	. . . . . . . 8 ⊢ (^◡𝐹:𝑆–1-1-onto→𝑅 → ^◡𝐹:𝑆⟶𝑅)
69	1, 67, 68	3syl 18	. . . . . . 7 ⊢ (𝜑 → ^◡𝐹:𝑆⟶𝑅)
70		ovex 7379	. . . . . . . . . 10 ⊢ ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
71	70	cnvex 7855	. . . . . . . . 9 ⊢ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
72	17, 71	fnmpoi 8002	. . . . . . . 8 ⊢ 𝐻 Fn (𝑆 × 𝑆)
73	72	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
74	33	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
75	69	ffvelcdmda 7017	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (^◡𝐹‘𝑢) ∈ 𝑅)
76	75	adantrr 717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑢) ∈ 𝑅)
77	69	ffvelcdmda 7017	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑣) ∈ 𝑅)
78	77	adantrl 716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑣) ∈ 𝑅)
79	30, 31, 32, 74, 76, 78	ffthf1o 17828	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
80		f1ocnv 6775	. . . . . . . . 9 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
81		f1of 6763	. . . . . . . . 9 ⊢ (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
82	79, 80, 81	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
83		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
84	83	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
85		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
86	85	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑣))
87	84, 86	oveq12d 7364	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
88	87	cnveqd 5814	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
89		ovex 7379	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
90	89	cnvex 7855	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
91	88, 17, 90	ovmpoa 7501	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
92	91	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
93	1	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹:𝑅–1-1-onto→𝑆)
94		simprl 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑢 ∈ 𝑆)
95		f1ocnvfv2 7211	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
96	93, 94, 95	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
97		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑣 ∈ 𝑆)
98		f1ocnvfv2 7211	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
99	93, 97, 98	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
100	96, 99	oveq12d 7364	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
101	100	eqcomd 2737	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢(Hom ‘𝑌)𝑣) = ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
102	92, 101	feq12d 6639	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) ↔ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))))
103	82, 102	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
104		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝑆)
105		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑥 = 𝑢)
106	105	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
107		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑦 = 𝑢)
108	107	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑢))
109	106, 108	oveq12d 7364	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
110	109	cnveqd 5814	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
111		ovex 7379	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
112	111	cnvex 7855	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
113	110, 17, 112	ovmpoa 7501	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
114	104, 104, 113	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
115	114	fveq1d 6824	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)))
116	51	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹(𝑋 Func 𝑌)𝐺)
117	30, 54, 53, 116, 75	funcid 17777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))))
118	1, 95	sylan 580	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
119	118	fveq2d 6826	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
120	117, 119	eqtrd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
121	33	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
122	30, 31, 32, 121, 75, 75	ffthf1o 17828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑢))))
123	66	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑋 ∈ Cat)
124	30, 31, 54, 123, 75	catidcl 17588	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑋)‘(^◡𝐹‘𝑢)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢)))
125		f1ocnvfv 7212	. . . . . . . . . 10 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑢))) ∧ ((Id‘𝑋)‘(^◡𝐹‘𝑢)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢))))
126	122, 124, 125	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢))))
127	120, 126	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢)))
128	115, 127	eqtrd 2766	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢)))
129	51	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹(𝑋 Func 𝑌)𝐺)
130	69	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡𝐹:𝑆⟶𝑅)
131		simp21 1207	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑢 ∈ 𝑆)
132	130, 131	ffvelcdmd 7018	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑢) ∈ 𝑅)
133		simp22 1208	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑣 ∈ 𝑆)
134	130, 133	ffvelcdmd 7018	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑣) ∈ 𝑅)
135		simp23 1209	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑧 ∈ 𝑆)
136	130, 135	ffvelcdmd 7018	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑧) ∈ 𝑅)
137	33	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
138	30, 31, 32, 137, 132, 134	ffthf1o 17828	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
139	1	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹:𝑅–1-1-onto→𝑆)
140	139, 131, 95	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
141	139, 133, 98	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
142	140, 141	oveq12d 7364	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
143	142	f1oeq3d 6760	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
144	138, 143	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
145		f1ocnv 6775	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
146		f1of 6763	. . . . . . . . . . . . 13 ⊢ (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
147	144, 145, 146	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
148		simp3l 1202	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣))
149	147, 148	ffvelcdmd 7018	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
150	30, 31, 32, 137, 134, 136	ffthf1o 17828	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
151		f1ocnvfv2 7211	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑧 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
152	139, 135, 151	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
153	141, 152	oveq12d 7364	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑣(Hom ‘𝑌)𝑧))
154	153	f1oeq3d 6760	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) ↔ ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧)))
155	150, 154	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧))
156		f1ocnv 6775	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
157		f1of 6763	. . . . . . . . . . . . 13 ⊢ (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
158	155, 156, 157	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
159		simp3r 1203	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))
160	158, 159	ffvelcdmd 7018	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔) ∈ ((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
161	30, 31, 56, 55, 129, 132, 134, 136, 149, 160	funcco 17778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
162	140, 141	opeq12d 4830	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩ = ⟨𝑢, 𝑣⟩)
163	162, 152	oveq12d 7364	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧))
164		f1ocnvfv2 7211	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧)) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
165	155, 159, 164	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
166		f1ocnvfv2 7211	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) ∧ 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣)) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
167	144, 148, 166	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
168	163, 165, 167	oveq123d 7367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
169	161, 168	eqtrd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
170	30, 31, 32, 137, 132, 136	ffthf1o 17828	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
171	140, 152	oveq12d 7364	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑢(Hom ‘𝑌)𝑧))
172	171	f1oeq3d 6760	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧)))
173	170, 172	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧))
174	66	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑋 ∈ Cat)
175	30, 31, 56, 174, 132, 134, 136, 149, 160	catcocl 17591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
176		f1ocnvfv 7212	. . . . . . . . . 10 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧) ∧ ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
177	173, 175, 176	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
178	169, 177	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)))
179		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑢)
180	179	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
181		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
182	181	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
183	180, 182	oveq12d 7364	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
184	183	cnveqd 5814	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
185		ovex 7379	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
186	185	cnvex 7855	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
187	184, 17, 186	ovmpoa 7501	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
188	131, 135, 187	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
189	188	fveq1d 6824	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)))
190		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑣)
191	190	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑣))
192		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
193	192	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
194	191, 193	oveq12d 7364	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
195	194	cnveqd 5814	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
196		ovex 7379	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
197	196	cnvex 7855	. . . . . . . . . . . 12 ⊢ ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
198	195, 17, 197	ovmpoa 7501	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
199	133, 135, 198	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
200	199	fveq1d 6824	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑣𝐻𝑧)‘𝑔) = (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))
201	131, 133, 91	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
202	201	fveq1d 6824	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑣)‘𝑓) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))
203	200, 202	oveq12d 7364	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)))
204	178, 189, 203	3eqtr4d 2776	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)))
205	52, 30, 32, 31, 53, 54, 55, 56, 64, 66, 69, 73, 103, 128, 204	isfuncd 17772	. . . . . 6 ⊢ (𝜑 → ^◡𝐹(𝑌 Func 𝑋)𝐻)
206	30, 51, 205	cofuval2 17794	. . . . 5 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩)
207		eqid 2731	. . . . . 6 ⊢ (id_func‘𝑋) = (id_func‘𝑋)
208	207, 30, 66, 31	idfuval 17783	. . . . 5 ⊢ (𝜑 → (id_func‘𝑋) = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
209	46, 206, 208	3eqtr4d 2776	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = (id_func‘𝑋))
210		eqid 2731	. . . . 5 ⊢ (comp‘𝐶) = (comp‘𝐶)
211		df-br 5090	. . . . . 6 ⊢ (𝐹(𝑋 Func 𝑌)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
212	51, 211	sylib 218	. . . . 5 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
213		df-br 5090	. . . . . 6 ⊢ (^◡𝐹(𝑌 Func 𝑋)𝐻 ↔ ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
214	205, 213	sylib 218	. . . . 5 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
215	57, 58, 59, 210, 65, 63, 65, 212, 214	catcco 18012	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩))
216		eqid 2731	. . . . 5 ⊢ (Id‘𝐶) = (Id‘𝐶)
217	57, 58, 216, 207, 59, 65	catcid 18014	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑋) = (id_func‘𝑋))
218	209, 215, 217	3eqtr4d 2776	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋))
219		eqid 2731	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
220		eqid 2731	. . . 4 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
221	57	catccat 18015	. . . . 5 ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
222	59, 221	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
223	57, 58, 59, 219, 65, 63	catchom 18010	. . . . 5 ⊢ (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌))
224	212, 223	eleqtrrd 2834	. . . 4 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋(Hom ‘𝐶)𝑌))
225	57, 58, 59, 219, 63, 65	catchom 18010	. . . . 5 ⊢ (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋))
226	214, 225	eleqtrrd 2834	. . . 4 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌(Hom ‘𝐶)𝑋))
227	58, 219, 210, 216, 220, 222, 65, 63, 224, 226	issect2 17661	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩ ↔ (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋)))
228	218, 227	mpbird 257	. 2 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩)
229		f1ococnv2 6790	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
230	1, 229	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
231	91	3adant1 1130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
232	231	coeq2d 5801	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)) = (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))))
233	33	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
234	75	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑢) ∈ 𝑅)
235	77	3adant2 1131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑣) ∈ 𝑅)
236	30, 31, 32, 233, 234, 235	ffthf1o 17828	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
237	100	3impb 1114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
238	237	f1oeq3d 6760	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
239	236, 238	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
240		f1ococnv2 6790	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
241	239, 240	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
242	232, 241	eqtrd 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
243	242	mpoeq3dva 7423	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣))))
244		fveq2 6822	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩))
245		df-ov 7349	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑌)𝑣) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩)
246	244, 245	eqtr4di 2784	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = (𝑢(Hom ‘𝑌)𝑣))
247	246	reseq2d 5927	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑌)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
248	247	mpompt 7460	. . . . . . 7 ⊢ (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
249	243, 248	eqtr4di 2784	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))))
250	230, 249	opeq12d 4830	. . . . 5 ⊢ (𝜑 → ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩ = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
251	52, 205, 51	cofuval2 17794	. . . . 5 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩)
252		eqid 2731	. . . . . 6 ⊢ (id_func‘𝑌) = (id_func‘𝑌)
253	252, 52, 64, 32	idfuval 17783	. . . . 5 ⊢ (𝜑 → (id_func‘𝑌) = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
254	250, 251, 253	3eqtr4d 2776	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = (id_func‘𝑌))
255	57, 58, 59, 210, 63, 65, 63, 214, 212	catcco 18012	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩))
256	57, 58, 216, 252, 59, 63	catcid 18014	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑌) = (id_func‘𝑌))
257	254, 255, 256	3eqtr4d 2776	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌))
258	58, 219, 210, 216, 220, 222, 63, 65, 226, 224	issect2 17661	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩ ↔ (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌)))
259	257, 258	mpbird 257	. 2 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)
260		catcisolem.i	. . 3 ⊢ 𝐼 = (Inv‘𝐶)
261	58, 260, 222, 65, 63, 220	isinv 17667	. 2 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨^◡𝐹, 𝐻⟩ ↔ (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩ ∧ ⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)))
262	228, 259, 261	mpbir2and 713	1 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨^◡𝐹, 𝐻⟩)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ∩ cin 3896 ⟨cop 4579 class class class wbr 5089 ↦ cmpt 5170 I cid 5508 × cxp 5612 ^◡ccnv 5613 ↾ cres 5616 ∘ ccom 5618 Fn wfn 6476 ⟶wf 6477 –1-1-onto→wf1o 6480 ‘cfv 6481 (class class class)co 7346 ∈ cmpo 7348 Basecbs 17120 Hom chom 17172 compcco 17173 Catccat 17570 Idccid 17571 Sectcsect 17651 Invcinv 17652 Func cfunc 17761 id_funccidfu 17762 ∘_func ccofu 17763 Full cful 17811 Faith cfth 17812 CatCatccatc 18005

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-map 8752 df-ixp 8822 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-5 12191 df-6 12192 df-7 12193 df-8 12194 df-9 12195 df-n0 12382 df-z 12469 df-dec 12589 df-uz 12733 df-fz 13408 df-struct 17058 df-slot 17093 df-ndx 17105 df-base 17121 df-hom 17185 df-cco 17186 df-cat 17574 df-cid 17575 df-sect 17654 df-inv 17655 df-func 17765 df-idfu 17766 df-cofu 17767 df-full 17813 df-fth 17814 df-catc 18006

This theorem is referenced by: catciso 18018

W3C validator