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 18163

Description: Lemma for catciso 18164. (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 6877	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
4	1	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅–1-1-onto→𝑆)
5		f1of 6848	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → 𝐹:𝑅⟶𝑆)
6	4, 5	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅⟶𝑆)
7		simp2 1136	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑢 ∈ 𝑅)
8	6, 7	ffvelcdmd 7104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑢) ∈ 𝑆)
9		simp3 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑣 ∈ 𝑅)
10	6, 9	ffvelcdmd 7104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑣) ∈ 𝑆)
11		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑥 = (𝐹‘𝑢))
12	11	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑥) = (^◡𝐹‘(𝐹‘𝑢)))
13		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑦 = (𝐹‘𝑣))
14	13	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑦) = (^◡𝐹‘(𝐹‘𝑣)))
15	12, 14	oveq12d 7448	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
16	15	cnveqd 5888	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
17		catcisolem.g	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)))
18		ovex 7463	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
19	18	cnvex 7947	. . . . . . . . . . . . 13 ⊢ ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
20	16, 17, 19	ovmpoa 7587	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑢) ∈ 𝑆 ∧ (𝐹‘𝑣) ∈ 𝑆) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
21	8, 10, 20	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
22		f1ocnvfv1 7295	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
23	4, 7, 22	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
24		f1ocnvfv1 7295	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
25	4, 9, 24	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
26	23, 25	oveq12d 7448	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = (𝑢𝐺𝑣))
27	26	cnveqd 5888	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = ^◡(𝑢𝐺𝑣))
28	21, 27	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡(𝑢𝐺𝑣))
29	28	coeq1d 5874	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)))
30		catciso.r	. . . . . . . . . . 11 ⊢ 𝑅 = (Base‘𝑋)
31		eqid 2734	. . . . . . . . . . 11 ⊢ (Hom ‘𝑋) = (Hom ‘𝑋)
32		eqid 2734	. . . . . . . . . . 11 ⊢ (Hom ‘𝑌) = (Hom ‘𝑌)
33		catcisolem.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
34	33	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
35	30, 31, 32, 34, 7, 9	ffthf1o 17972	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)))
36		f1ococnv1 6877	. . . . . . . . . 10 ⊢ ((𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
37	35, 36	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
38	29, 37	eqtrd 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
39	38	mpoeq3dva 7509	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣))))
40		fveq2 6906	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩))
41		df-ov 7433	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑋)𝑣) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩)
42	40, 41	eqtr4di 2792	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = (𝑢(Hom ‘𝑋)𝑣))
43	42	reseq2d 5999	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑋)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
44	43	mpompt 7546	. . . . . . 7 ⊢ (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
45	39, 44	eqtr4di 2792	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))))
46	3, 45	opeq12d 4885	. . . . 5 ⊢ (𝜑 → ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩ = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
47		inss1 4244	. . . . . . . . 9 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Full 𝑌)
48		fullfunc 17959	. . . . . . . . 9 ⊢ (𝑋 Full 𝑌) ⊆ (𝑋 Func 𝑌)
49	47, 48	sstri 4004	. . . . . . . 8 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Func 𝑌)
50	49	ssbri 5192	. . . . . . 7 ⊢ (𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺 → 𝐹(𝑋 Func 𝑌)𝐺)
51	33, 50	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹(𝑋 Func 𝑌)𝐺)
52		catciso.s	. . . . . . 7 ⊢ 𝑆 = (Base‘𝑌)
53		eqid 2734	. . . . . . 7 ⊢ (Id‘𝑌) = (Id‘𝑌)
54		eqid 2734	. . . . . . 7 ⊢ (Id‘𝑋) = (Id‘𝑋)
55		eqid 2734	. . . . . . 7 ⊢ (comp‘𝑌) = (comp‘𝑌)
56		eqid 2734	. . . . . . 7 ⊢ (comp‘𝑋) = (comp‘𝑋)
57		catciso.c	. . . . . . . . . 10 ⊢ 𝐶 = (CatCat‘𝑈)
58		catciso.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
59		catciso.u	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
60	57, 58, 59	catcbas 18154	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
61		inss2 4245	. . . . . . . . 9 ⊢ (𝑈 ∩ Cat) ⊆ Cat
62	60, 61	eqsstrdi 4049	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ Cat)
63		catciso.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
64	62, 63	sseldd 3995	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ Cat)
65		catciso.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
66	62, 65	sseldd 3995	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Cat)
67		f1ocnv 6860	. . . . . . . 8 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → ^◡𝐹:𝑆–1-1-onto→𝑅)
68		f1of 6848	. . . . . . . 8 ⊢ (^◡𝐹:𝑆–1-1-onto→𝑅 → ^◡𝐹:𝑆⟶𝑅)
69	1, 67, 68	3syl 18	. . . . . . 7 ⊢ (𝜑 → ^◡𝐹:𝑆⟶𝑅)
70		ovex 7463	. . . . . . . . . 10 ⊢ ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
71	70	cnvex 7947	. . . . . . . . 9 ⊢ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
72	17, 71	fnmpoi 8093	. . . . . . . 8 ⊢ 𝐻 Fn (𝑆 × 𝑆)
73	72	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
74	33	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
75	69	ffvelcdmda 7103	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (^◡𝐹‘𝑢) ∈ 𝑅)
76	75	adantrr 717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑢) ∈ 𝑅)
77	69	ffvelcdmda 7103	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑣) ∈ 𝑅)
78	77	adantrl 716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑣) ∈ 𝑅)
79	30, 31, 32, 74, 76, 78	ffthf1o 17972	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
80		f1ocnv 6860	. . . . . . . . 9 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
81		f1of 6848	. . . . . . . . 9 ⊢ (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
82	79, 80, 81	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
83		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
84	83	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
85		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
86	85	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑣))
87	84, 86	oveq12d 7448	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
88	87	cnveqd 5888	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
89		ovex 7463	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
90	89	cnvex 7947	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
91	88, 17, 90	ovmpoa 7587	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
92	91	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
93	1	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹:𝑅–1-1-onto→𝑆)
94		simprl 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑢 ∈ 𝑆)
95		f1ocnvfv2 7296	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
96	93, 94, 95	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
97		simprr 773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑣 ∈ 𝑆)
98		f1ocnvfv2 7296	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
99	93, 97, 98	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
100	96, 99	oveq12d 7448	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
101	100	eqcomd 2740	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢(Hom ‘𝑌)𝑣) = ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
102	92, 101	feq12d 6724	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) ↔ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))))
103	82, 102	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
104		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝑆)
105		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑥 = 𝑢)
106	105	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
107		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑦 = 𝑢)
108	107	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑢))
109	106, 108	oveq12d 7448	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
110	109	cnveqd 5888	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
111		ovex 7463	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
112	111	cnvex 7947	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
113	110, 17, 112	ovmpoa 7587	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
114	104, 104, 113	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
115	114	fveq1d 6908	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)))
116	51	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹(𝑋 Func 𝑌)𝐺)
117	30, 54, 53, 116, 75	funcid 17920	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))))
118	1, 95	sylan 580	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
119	118	fveq2d 6910	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
120	117, 119	eqtrd 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
121	33	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
122	30, 31, 32, 121, 75, 75	ffthf1o 17972	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑢))))
123	66	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑋 ∈ Cat)
124	30, 31, 54, 123, 75	catidcl 17726	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑋)‘(^◡𝐹‘𝑢)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢)))
125		f1ocnvfv 7297	. . . . . . . . . 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 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢)))
129	51	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹(𝑋 Func 𝑌)𝐺)
130	69	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡𝐹:𝑆⟶𝑅)
131		simp21 1205	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑢 ∈ 𝑆)
132	130, 131	ffvelcdmd 7104	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑢) ∈ 𝑅)
133		simp22 1206	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑣 ∈ 𝑆)
134	130, 133	ffvelcdmd 7104	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑣) ∈ 𝑅)
135		simp23 1207	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑧 ∈ 𝑆)
136	130, 135	ffvelcdmd 7104	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑧) ∈ 𝑅)
137	33	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
138	30, 31, 32, 137, 132, 134	ffthf1o 17972	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
139	1	3ad2ant1 1132	. . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
143	142	f1oeq3d 6845	. . . . . . . . . . . . . 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 6860	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
146		f1of 6848	. . . . . . . . . . . . 13 ⊢ (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
147	144, 145, 146	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
148		simp3l 1200	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣))
149	147, 148	ffvelcdmd 7104	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
150	30, 31, 32, 137, 134, 136	ffthf1o 17972	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
151		f1ocnvfv2 7296	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑧 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
152	139, 135, 151	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
153	141, 152	oveq12d 7448	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑣(Hom ‘𝑌)𝑧))
154	153	f1oeq3d 6845	. . . . . . . . . . . . . 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 6860	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
157		f1of 6848	. . . . . . . . . . . . 13 ⊢ (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
158	155, 156, 157	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
159		simp3r 1201	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))
160	158, 159	ffvelcdmd 7104	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔) ∈ ((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
161	30, 31, 56, 55, 129, 132, 134, 136, 149, 160	funcco 17921	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
162	140, 141	opeq12d 4885	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩ = ⟨𝑢, 𝑣⟩)
163	162, 152	oveq12d 7448	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧))
164		f1ocnvfv2 7296	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧)) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
165	155, 159, 164	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
166		f1ocnvfv2 7296	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) ∧ 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣)) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
167	144, 148, 166	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
168	163, 165, 167	oveq123d 7451	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
169	161, 168	eqtrd 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
170	30, 31, 32, 137, 132, 136	ffthf1o 17972	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
171	140, 152	oveq12d 7448	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑢(Hom ‘𝑌)𝑧))
172	171	f1oeq3d 6845	. . . . . . . . . . 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 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑋 ∈ Cat)
175	30, 31, 56, 174, 132, 134, 136, 149, 160	catcocl 17729	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
176		f1ocnvfv 7297	. . . . . . . . . 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 6910	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
181		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
182	181	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
183	180, 182	oveq12d 7448	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
184	183	cnveqd 5888	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
185		ovex 7463	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
186	185	cnvex 7947	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
187	184, 17, 186	ovmpoa 7587	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
188	131, 135, 187	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
189	188	fveq1d 6908	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)))
190		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑣)
191	190	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑣))
192		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
193	192	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
194	191, 193	oveq12d 7448	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
195	194	cnveqd 5888	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
196		ovex 7463	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
197	196	cnvex 7947	. . . . . . . . . . . 12 ⊢ ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
198	195, 17, 197	ovmpoa 7587	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
199	133, 135, 198	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
200	199	fveq1d 6908	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑣𝐻𝑧)‘𝑔) = (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))
201	131, 133, 91	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
202	201	fveq1d 6908	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑣)‘𝑓) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))
203	200, 202	oveq12d 7448	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)))
204	178, 189, 203	3eqtr4d 2784	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)))
205	52, 30, 32, 31, 53, 54, 55, 56, 64, 66, 69, 73, 103, 128, 204	isfuncd 17915	. . . . . 6 ⊢ (𝜑 → ^◡𝐹(𝑌 Func 𝑋)𝐻)
206	30, 51, 205	cofuval2 17937	. . . . 5 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩)
207		eqid 2734	. . . . . 6 ⊢ (id_func‘𝑋) = (id_func‘𝑋)
208	207, 30, 66, 31	idfuval 17926	. . . . 5 ⊢ (𝜑 → (id_func‘𝑋) = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
209	46, 206, 208	3eqtr4d 2784	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = (id_func‘𝑋))
210		eqid 2734	. . . . 5 ⊢ (comp‘𝐶) = (comp‘𝐶)
211		df-br 5148	. . . . . 6 ⊢ (𝐹(𝑋 Func 𝑌)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
212	51, 211	sylib 218	. . . . 5 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
213		df-br 5148	. . . . . 6 ⊢ (^◡𝐹(𝑌 Func 𝑋)𝐻 ↔ ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
214	205, 213	sylib 218	. . . . 5 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
215	57, 58, 59, 210, 65, 63, 65, 212, 214	catcco 18158	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩))
216		eqid 2734	. . . . 5 ⊢ (Id‘𝐶) = (Id‘𝐶)
217	57, 58, 216, 207, 59, 65	catcid 18160	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑋) = (id_func‘𝑋))
218	209, 215, 217	3eqtr4d 2784	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋))
219		eqid 2734	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
220		eqid 2734	. . . 4 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
221	57	catccat 18161	. . . . 5 ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
222	59, 221	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
223	57, 58, 59, 219, 65, 63	catchom 18156	. . . . 5 ⊢ (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌))
224	212, 223	eleqtrrd 2841	. . . 4 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋(Hom ‘𝐶)𝑌))
225	57, 58, 59, 219, 63, 65	catchom 18156	. . . . 5 ⊢ (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋))
226	214, 225	eleqtrrd 2841	. . . 4 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌(Hom ‘𝐶)𝑋))
227	58, 219, 210, 216, 220, 222, 65, 63, 224, 226	issect2 17801	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩ ↔ (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋)))
228	218, 227	mpbird 257	. 2 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩)
229		f1ococnv2 6875	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
230	1, 229	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
231	91	3adant1 1129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
232	231	coeq2d 5875	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)) = (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))))
233	33	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
234	75	3adant3 1131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑢) ∈ 𝑅)
235	77	3adant2 1130	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑣) ∈ 𝑅)
236	30, 31, 32, 233, 234, 235	ffthf1o 17972	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
237	100	3impb 1114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
238	237	f1oeq3d 6845	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
239	236, 238	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
240		f1ococnv2 6875	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
241	239, 240	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
242	232, 241	eqtrd 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
243	242	mpoeq3dva 7509	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣))))
244		fveq2 6906	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩))
245		df-ov 7433	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑌)𝑣) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩)
246	244, 245	eqtr4di 2792	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = (𝑢(Hom ‘𝑌)𝑣))
247	246	reseq2d 5999	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑌)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
248	247	mpompt 7546	. . . . . . 7 ⊢ (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
249	243, 248	eqtr4di 2792	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))))
250	230, 249	opeq12d 4885	. . . . 5 ⊢ (𝜑 → ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩ = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
251	52, 205, 51	cofuval2 17937	. . . . 5 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩)
252		eqid 2734	. . . . . 6 ⊢ (id_func‘𝑌) = (id_func‘𝑌)
253	252, 52, 64, 32	idfuval 17926	. . . . 5 ⊢ (𝜑 → (id_func‘𝑌) = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
254	250, 251, 253	3eqtr4d 2784	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = (id_func‘𝑌))
255	57, 58, 59, 210, 63, 65, 63, 214, 212	catcco 18158	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩))
256	57, 58, 216, 252, 59, 63	catcid 18160	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑌) = (id_func‘𝑌))
257	254, 255, 256	3eqtr4d 2784	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌))
258	58, 219, 210, 216, 220, 222, 63, 65, 226, 224	issect2 17801	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩ ↔ (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌)))
259	257, 258	mpbird 257	. 2 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)
260		catcisolem.i	. . 3 ⊢ 𝐼 = (Inv‘𝐶)
261	58, 260, 222, 65, 63, 220	isinv 17807	. 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 1536 ∈ wcel 2105 ∩ cin 3961 ⟨cop 4636 class class class wbr 5147 ↦ cmpt 5230 I cid 5581 × cxp 5686 ^◡ccnv 5687 ↾ cres 5690 ∘ ccom 5692 Fn wfn 6557 ⟶wf 6558 –1-1-onto→wf1o 6561 ‘cfv 6562 (class class class)co 7430 ∈ cmpo 7432 Basecbs 17244 Hom chom 17308 compcco 17309 Catccat 17708 Idccid 17709 Sectcsect 17791 Invcinv 17792 Func cfunc 17904 id_funccidfu 17905 ∘_func ccofu 17906 Full cful 17955 Faith cfth 17956 CatCatccatc 18151

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4912 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7887 df-1st 8012 df-2nd 8013 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-1o 8504 df-er 8743 df-map 8866 df-ixp 8936 df-en 8984 df-dom 8985 df-sdom 8986 df-fin 8987 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-nn 12264 df-2 12326 df-3 12327 df-4 12328 df-5 12329 df-6 12330 df-7 12331 df-8 12332 df-9 12333 df-n0 12524 df-z 12611 df-dec 12731 df-uz 12876 df-fz 13544 df-struct 17180 df-slot 17215 df-ndx 17227 df-base 17245 df-hom 17321 df-cco 17322 df-cat 17712 df-cid 17713 df-sect 17794 df-inv 17795 df-func 17908 df-idfu 17909 df-cofu 17910 df-full 17957 df-fth 17958 df-catc 18152

This theorem is referenced by: catciso 18164

W3C validator