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 17432

Description: Lemma for catciso 17433. (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 6630	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
4	1	3ad2ant1 1130	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅–1-1-onto→𝑆)
5		f1of 6602	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → 𝐹:𝑅⟶𝑆)
6	4, 5	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅⟶𝑆)
7		simp2 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑢 ∈ 𝑅)
8	6, 7	ffvelrnd 6843	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑢) ∈ 𝑆)
9		simp3 1135	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑣 ∈ 𝑅)
10	6, 9	ffvelrnd 6843	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑣) ∈ 𝑆)
11		simpl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑥 = (𝐹‘𝑢))
12	11	fveq2d 6662	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑥) = (^◡𝐹‘(𝐹‘𝑢)))
13		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑦 = (𝐹‘𝑣))
14	13	fveq2d 6662	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑦) = (^◡𝐹‘(𝐹‘𝑣)))
15	12, 14	oveq12d 7168	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
16	15	cnveqd 5715	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
17		catcisolem.g	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)))
18		ovex 7183	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
19	18	cnvex 7635	. . . . . . . . . . . . 13 ⊢ ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
20	16, 17, 19	ovmpoa 7300	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑢) ∈ 𝑆 ∧ (𝐹‘𝑣) ∈ 𝑆) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
21	8, 10, 20	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
22		f1ocnvfv1 7025	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
23	4, 7, 22	syl2anc 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
24		f1ocnvfv1 7025	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
25	4, 9, 24	syl2anc 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
26	23, 25	oveq12d 7168	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = (𝑢𝐺𝑣))
27	26	cnveqd 5715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = ^◡(𝑢𝐺𝑣))
28	21, 27	eqtrd 2793	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡(𝑢𝐺𝑣))
29	28	coeq1d 5701	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)))
30		catciso.r	. . . . . . . . . . 11 ⊢ 𝑅 = (Base‘𝑋)
31		eqid 2758	. . . . . . . . . . 11 ⊢ (Hom ‘𝑋) = (Hom ‘𝑋)
32		eqid 2758	. . . . . . . . . . 11 ⊢ (Hom ‘𝑌) = (Hom ‘𝑌)
33		catcisolem.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
34	33	3ad2ant1 1130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
35	30, 31, 32, 34, 7, 9	ffthf1o 17248	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)))
36		f1ococnv1 6630	. . . . . . . . . 10 ⊢ ((𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
37	35, 36	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
38	29, 37	eqtrd 2793	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
39	38	mpoeq3dva 7225	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣))))
40		fveq2 6658	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩))
41		df-ov 7153	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑋)𝑣) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩)
42	40, 41	eqtr4di 2811	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = (𝑢(Hom ‘𝑋)𝑣))
43	42	reseq2d 5823	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑋)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
44	43	mpompt 7260	. . . . . . 7 ⊢ (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
45	39, 44	eqtr4di 2811	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))))
46	3, 45	opeq12d 4771	. . . . 5 ⊢ (𝜑 → ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩ = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
47		inss1 4133	. . . . . . . . 9 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Full 𝑌)
48		fullfunc 17235	. . . . . . . . 9 ⊢ (𝑋 Full 𝑌) ⊆ (𝑋 Func 𝑌)
49	47, 48	sstri 3901	. . . . . . . 8 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Func 𝑌)
50	49	ssbri 5077	. . . . . . 7 ⊢ (𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺 → 𝐹(𝑋 Func 𝑌)𝐺)
51	33, 50	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹(𝑋 Func 𝑌)𝐺)
52		catciso.s	. . . . . . 7 ⊢ 𝑆 = (Base‘𝑌)
53		eqid 2758	. . . . . . 7 ⊢ (Id‘𝑌) = (Id‘𝑌)
54		eqid 2758	. . . . . . 7 ⊢ (Id‘𝑋) = (Id‘𝑋)
55		eqid 2758	. . . . . . 7 ⊢ (comp‘𝑌) = (comp‘𝑌)
56		eqid 2758	. . . . . . 7 ⊢ (comp‘𝑋) = (comp‘𝑋)
57		catciso.c	. . . . . . . . . 10 ⊢ 𝐶 = (CatCat‘𝑈)
58		catciso.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
59		catciso.u	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
60	57, 58, 59	catcbas 17423	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
61		inss2 4134	. . . . . . . . 9 ⊢ (𝑈 ∩ Cat) ⊆ Cat
62	60, 61	eqsstrdi 3946	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ Cat)
63		catciso.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
64	62, 63	sseldd 3893	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ Cat)
65		catciso.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
66	62, 65	sseldd 3893	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Cat)
67		f1ocnv 6614	. . . . . . . 8 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → ^◡𝐹:𝑆–1-1-onto→𝑅)
68		f1of 6602	. . . . . . . 8 ⊢ (^◡𝐹:𝑆–1-1-onto→𝑅 → ^◡𝐹:𝑆⟶𝑅)
69	1, 67, 68	3syl 18	. . . . . . 7 ⊢ (𝜑 → ^◡𝐹:𝑆⟶𝑅)
70		ovex 7183	. . . . . . . . . 10 ⊢ ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
71	70	cnvex 7635	. . . . . . . . 9 ⊢ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
72	17, 71	fnmpoi 7772	. . . . . . . 8 ⊢ 𝐻 Fn (𝑆 × 𝑆)
73	72	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
74	33	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
75	69	ffvelrnda 6842	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (^◡𝐹‘𝑢) ∈ 𝑅)
76	75	adantrr 716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑢) ∈ 𝑅)
77	69	ffvelrnda 6842	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑣) ∈ 𝑅)
78	77	adantrl 715	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑣) ∈ 𝑅)
79	30, 31, 32, 74, 76, 78	ffthf1o 17248	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
80		f1ocnv 6614	. . . . . . . . 9 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
81		f1of 6602	. . . . . . . . 9 ⊢ (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
82	79, 80, 81	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
83		simpl 486	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
84	83	fveq2d 6662	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
85		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
86	85	fveq2d 6662	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑣))
87	84, 86	oveq12d 7168	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
88	87	cnveqd 5715	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
89		ovex 7183	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
90	89	cnvex 7635	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
91	88, 17, 90	ovmpoa 7300	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
92	91	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
93	1	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹:𝑅–1-1-onto→𝑆)
94		simprl 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑢 ∈ 𝑆)
95		f1ocnvfv2 7026	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
96	93, 94, 95	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
97		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑣 ∈ 𝑆)
98		f1ocnvfv2 7026	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
99	93, 97, 98	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
100	96, 99	oveq12d 7168	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
101	100	eqcomd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢(Hom ‘𝑌)𝑣) = ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
102	92, 101	feq12d 6486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) ↔ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))))
103	82, 102	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
104		simpr 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝑆)
105		simpl 486	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑥 = 𝑢)
106	105	fveq2d 6662	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
107		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑦 = 𝑢)
108	107	fveq2d 6662	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑢))
109	106, 108	oveq12d 7168	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
110	109	cnveqd 5715	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
111		ovex 7183	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
112	111	cnvex 7635	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
113	110, 17, 112	ovmpoa 7300	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
114	104, 104, 113	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
115	114	fveq1d 6660	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)))
116	51	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹(𝑋 Func 𝑌)𝐺)
117	30, 54, 53, 116, 75	funcid 17199	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))))
118	1, 95	sylan 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
119	118	fveq2d 6662	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
120	117, 119	eqtrd 2793	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
121	33	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
122	30, 31, 32, 121, 75, 75	ffthf1o 17248	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑢))))
123	66	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑋 ∈ Cat)
124	30, 31, 54, 123, 75	catidcl 17011	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑋)‘(^◡𝐹‘𝑢)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢)))
125		f1ocnvfv 7027	. . . . . . . . . 10 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑢))) ∧ ((Id‘𝑋)‘(^◡𝐹‘𝑢)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢))))
126	122, 124, 125	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢))))
127	120, 126	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢)))
128	115, 127	eqtrd 2793	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢)))
129	51	3ad2ant1 1130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹(𝑋 Func 𝑌)𝐺)
130	69	3ad2ant1 1130	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡𝐹:𝑆⟶𝑅)
131		simp21 1203	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑢 ∈ 𝑆)
132	130, 131	ffvelrnd 6843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑢) ∈ 𝑅)
133		simp22 1204	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑣 ∈ 𝑆)
134	130, 133	ffvelrnd 6843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑣) ∈ 𝑅)
135		simp23 1205	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑧 ∈ 𝑆)
136	130, 135	ffvelrnd 6843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑧) ∈ 𝑅)
137	33	3ad2ant1 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
138	30, 31, 32, 137, 132, 134	ffthf1o 17248	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
139	1	3ad2ant1 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹:𝑅–1-1-onto→𝑆)
140	139, 131, 95	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
141	139, 133, 98	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
142	140, 141	oveq12d 7168	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
143	142	f1oeq3d 6599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
144	138, 143	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
145		f1ocnv 6614	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
146		f1of 6602	. . . . . . . . . . . . 13 ⊢ (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
147	144, 145, 146	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
148		simp3l 1198	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣))
149	147, 148	ffvelrnd 6843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
150	30, 31, 32, 137, 134, 136	ffthf1o 17248	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
151		f1ocnvfv2 7026	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑧 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
152	139, 135, 151	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
153	141, 152	oveq12d 7168	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑣(Hom ‘𝑌)𝑧))
154	153	f1oeq3d 6599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) ↔ ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧)))
155	150, 154	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧))
156		f1ocnv 6614	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
157		f1of 6602	. . . . . . . . . . . . 13 ⊢ (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
158	155, 156, 157	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
159		simp3r 1199	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))
160	158, 159	ffvelrnd 6843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔) ∈ ((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
161	30, 31, 56, 55, 129, 132, 134, 136, 149, 160	funcco 17200	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
162	140, 141	opeq12d 4771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩ = ⟨𝑢, 𝑣⟩)
163	162, 152	oveq12d 7168	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧))
164		f1ocnvfv2 7026	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧)) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
165	155, 159, 164	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
166		f1ocnvfv2 7026	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) ∧ 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣)) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
167	144, 148, 166	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
168	163, 165, 167	oveq123d 7171	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
169	161, 168	eqtrd 2793	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
170	30, 31, 32, 137, 132, 136	ffthf1o 17248	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
171	140, 152	oveq12d 7168	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑢(Hom ‘𝑌)𝑧))
172	171	f1oeq3d 6599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧)))
173	170, 172	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧))
174	66	3ad2ant1 1130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑋 ∈ Cat)
175	30, 31, 56, 174, 132, 134, 136, 149, 160	catcocl 17014	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
176		f1ocnvfv 7027	. . . . . . . . . 10 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧) ∧ ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
177	173, 175, 176	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
178	169, 177	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)))
179		simpl 486	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑢)
180	179	fveq2d 6662	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
181		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
182	181	fveq2d 6662	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
183	180, 182	oveq12d 7168	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
184	183	cnveqd 5715	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
185		ovex 7183	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
186	185	cnvex 7635	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
187	184, 17, 186	ovmpoa 7300	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
188	131, 135, 187	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
189	188	fveq1d 6660	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)))
190		simpl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑣)
191	190	fveq2d 6662	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑣))
192		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
193	192	fveq2d 6662	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
194	191, 193	oveq12d 7168	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
195	194	cnveqd 5715	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
196		ovex 7183	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
197	196	cnvex 7635	. . . . . . . . . . . 12 ⊢ ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
198	195, 17, 197	ovmpoa 7300	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
199	133, 135, 198	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
200	199	fveq1d 6660	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑣𝐻𝑧)‘𝑔) = (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))
201	131, 133, 91	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
202	201	fveq1d 6660	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑣)‘𝑓) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))
203	200, 202	oveq12d 7168	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)))
204	178, 189, 203	3eqtr4d 2803	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)))
205	52, 30, 32, 31, 53, 54, 55, 56, 64, 66, 69, 73, 103, 128, 204	isfuncd 17194	. . . . . 6 ⊢ (𝜑 → ^◡𝐹(𝑌 Func 𝑋)𝐻)
206	30, 51, 205	cofuval2 17216	. . . . 5 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩)
207		eqid 2758	. . . . . 6 ⊢ (id_func‘𝑋) = (id_func‘𝑋)
208	207, 30, 66, 31	idfuval 17205	. . . . 5 ⊢ (𝜑 → (id_func‘𝑋) = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
209	46, 206, 208	3eqtr4d 2803	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = (id_func‘𝑋))
210		eqid 2758	. . . . 5 ⊢ (comp‘𝐶) = (comp‘𝐶)
211		df-br 5033	. . . . . 6 ⊢ (𝐹(𝑋 Func 𝑌)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
212	51, 211	sylib 221	. . . . 5 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
213		df-br 5033	. . . . . 6 ⊢ (^◡𝐹(𝑌 Func 𝑋)𝐻 ↔ ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
214	205, 213	sylib 221	. . . . 5 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
215	57, 58, 59, 210, 65, 63, 65, 212, 214	catcco 17427	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩))
216		eqid 2758	. . . . 5 ⊢ (Id‘𝐶) = (Id‘𝐶)
217	57, 58, 216, 207, 59, 65	catcid 17429	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑋) = (id_func‘𝑋))
218	209, 215, 217	3eqtr4d 2803	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋))
219		eqid 2758	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
220		eqid 2758	. . . 4 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
221	57	catccat 17430	. . . . 5 ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
222	59, 221	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
223	57, 58, 59, 219, 65, 63	catchom 17425	. . . . 5 ⊢ (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌))
224	212, 223	eleqtrrd 2855	. . . 4 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋(Hom ‘𝐶)𝑌))
225	57, 58, 59, 219, 63, 65	catchom 17425	. . . . 5 ⊢ (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋))
226	214, 225	eleqtrrd 2855	. . . 4 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌(Hom ‘𝐶)𝑋))
227	58, 219, 210, 216, 220, 222, 65, 63, 224, 226	issect2 17083	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩ ↔ (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋)))
228	218, 227	mpbird 260	. 2 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩)
229		f1ococnv2 6628	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
230	1, 229	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
231	91	3adant1 1127	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
232	231	coeq2d 5702	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)) = (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))))
233	33	3ad2ant1 1130	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
234	75	3adant3 1129	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑢) ∈ 𝑅)
235	77	3adant2 1128	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑣) ∈ 𝑅)
236	30, 31, 32, 233, 234, 235	ffthf1o 17248	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
237	100	3impb 1112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
238	237	f1oeq3d 6599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
239	236, 238	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
240		f1ococnv2 6628	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
241	239, 240	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
242	232, 241	eqtrd 2793	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
243	242	mpoeq3dva 7225	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣))))
244		fveq2 6658	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩))
245		df-ov 7153	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑌)𝑣) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩)
246	244, 245	eqtr4di 2811	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = (𝑢(Hom ‘𝑌)𝑣))
247	246	reseq2d 5823	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑌)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
248	247	mpompt 7260	. . . . . . 7 ⊢ (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
249	243, 248	eqtr4di 2811	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))))
250	230, 249	opeq12d 4771	. . . . 5 ⊢ (𝜑 → ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩ = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
251	52, 205, 51	cofuval2 17216	. . . . 5 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩)
252		eqid 2758	. . . . . 6 ⊢ (id_func‘𝑌) = (id_func‘𝑌)
253	252, 52, 64, 32	idfuval 17205	. . . . 5 ⊢ (𝜑 → (id_func‘𝑌) = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
254	250, 251, 253	3eqtr4d 2803	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = (id_func‘𝑌))
255	57, 58, 59, 210, 63, 65, 63, 214, 212	catcco 17427	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩))
256	57, 58, 216, 252, 59, 63	catcid 17429	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑌) = (id_func‘𝑌))
257	254, 255, 256	3eqtr4d 2803	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌))
258	58, 219, 210, 216, 220, 222, 63, 65, 226, 224	issect2 17083	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩ ↔ (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌)))
259	257, 258	mpbird 260	. 2 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)
260		catcisolem.i	. . 3 ⊢ 𝐼 = (Inv‘𝐶)
261	58, 260, 222, 65, 63, 220	isinv 17089	. 2 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨^◡𝐹, 𝐻⟩ ↔ (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩ ∧ ⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)))
262	228, 259, 261	mpbir2and 712	1 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨^◡𝐹, 𝐻⟩)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∩ cin 3857 ⟨cop 4528 class class class wbr 5032 ↦ cmpt 5112 I cid 5429 × cxp 5522 ^◡ccnv 5523 ↾ cres 5526 ∘ ccom 5528 Fn wfn 6330 ⟶wf 6331 –1-1-onto→wf1o 6334 ‘cfv 6335 (class class class)co 7150 ∈ cmpo 7152 Basecbs 16541 Hom chom 16634 compcco 16635 Catccat 16993 Idccid 16994 Sectcsect 17073 Invcinv 17074 Func cfunc 17183 id_funccidfu 17184 ∘_func ccofu 17185 Full cful 17231 Faith cfth 17232 CatCatccatc 17420

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5156 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-uni 4799 df-iun 4885 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7580 df-1st 7693 df-2nd 7694 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-1o 8112 df-er 8299 df-map 8418 df-ixp 8480 df-en 8528 df-dom 8529 df-sdom 8530 df-fin 8531 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-nn 11675 df-2 11737 df-3 11738 df-4 11739 df-5 11740 df-6 11741 df-7 11742 df-8 11743 df-9 11744 df-n0 11935 df-z 12021 df-dec 12138 df-uz 12283 df-fz 12940 df-struct 16543 df-ndx 16544 df-slot 16545 df-base 16547 df-hom 16647 df-cco 16648 df-cat 16997 df-cid 16998 df-sect 17076 df-inv 17077 df-func 17187 df-idfu 17188 df-cofu 17189 df-full 17233 df-fth 17234 df-catc 17421

This theorem is referenced by: catciso 17433

W3C validator