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 17825

Description: Lemma for catciso 17826. (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 6745	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
4	1	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅–1-1-onto→𝑆)
5		f1of 6716	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → 𝐹:𝑅⟶𝑆)
6	4, 5	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅⟶𝑆)
7		simp2 1136	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑢 ∈ 𝑅)
8	6, 7	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑢) ∈ 𝑆)
9		simp3 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑣 ∈ 𝑅)
10	6, 9	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑣) ∈ 𝑆)
11		simpl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑥 = (𝐹‘𝑢))
12	11	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑥) = (^◡𝐹‘(𝐹‘𝑢)))
13		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑦 = (𝐹‘𝑣))
14	13	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑦) = (^◡𝐹‘(𝐹‘𝑣)))
15	12, 14	oveq12d 7293	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
16	15	cnveqd 5784	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
17		catcisolem.g	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)))
18		ovex 7308	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
19	18	cnvex 7772	. . . . . . . . . . . . 13 ⊢ ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
20	16, 17, 19	ovmpoa 7428	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑢) ∈ 𝑆 ∧ (𝐹‘𝑣) ∈ 𝑆) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
21	8, 10, 20	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
22		f1ocnvfv1 7148	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
23	4, 7, 22	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
24		f1ocnvfv1 7148	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
25	4, 9, 24	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
26	23, 25	oveq12d 7293	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = (𝑢𝐺𝑣))
27	26	cnveqd 5784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = ^◡(𝑢𝐺𝑣))
28	21, 27	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡(𝑢𝐺𝑣))
29	28	coeq1d 5770	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)))
30		catciso.r	. . . . . . . . . . 11 ⊢ 𝑅 = (Base‘𝑋)
31		eqid 2738	. . . . . . . . . . 11 ⊢ (Hom ‘𝑋) = (Hom ‘𝑋)
32		eqid 2738	. . . . . . . . . . 11 ⊢ (Hom ‘𝑌) = (Hom ‘𝑌)
33		catcisolem.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
34	33	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
35	30, 31, 32, 34, 7, 9	ffthf1o 17635	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)))
36		f1ococnv1 6745	. . . . . . . . . 10 ⊢ ((𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
37	35, 36	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
38	29, 37	eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
39	38	mpoeq3dva 7352	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣))))
40		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩))
41		df-ov 7278	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑋)𝑣) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩)
42	40, 41	eqtr4di 2796	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = (𝑢(Hom ‘𝑋)𝑣))
43	42	reseq2d 5891	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑋)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
44	43	mpompt 7388	. . . . . . 7 ⊢ (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
45	39, 44	eqtr4di 2796	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))))
46	3, 45	opeq12d 4812	. . . . 5 ⊢ (𝜑 → ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩ = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
47		inss1 4162	. . . . . . . . 9 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Full 𝑌)
48		fullfunc 17622	. . . . . . . . 9 ⊢ (𝑋 Full 𝑌) ⊆ (𝑋 Func 𝑌)
49	47, 48	sstri 3930	. . . . . . . 8 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Func 𝑌)
50	49	ssbri 5119	. . . . . . 7 ⊢ (𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺 → 𝐹(𝑋 Func 𝑌)𝐺)
51	33, 50	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹(𝑋 Func 𝑌)𝐺)
52		catciso.s	. . . . . . 7 ⊢ 𝑆 = (Base‘𝑌)
53		eqid 2738	. . . . . . 7 ⊢ (Id‘𝑌) = (Id‘𝑌)
54		eqid 2738	. . . . . . 7 ⊢ (Id‘𝑋) = (Id‘𝑋)
55		eqid 2738	. . . . . . 7 ⊢ (comp‘𝑌) = (comp‘𝑌)
56		eqid 2738	. . . . . . 7 ⊢ (comp‘𝑋) = (comp‘𝑋)
57		catciso.c	. . . . . . . . . 10 ⊢ 𝐶 = (CatCat‘𝑈)
58		catciso.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
59		catciso.u	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
60	57, 58, 59	catcbas 17816	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
61		inss2 4163	. . . . . . . . 9 ⊢ (𝑈 ∩ Cat) ⊆ Cat
62	60, 61	eqsstrdi 3975	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ Cat)
63		catciso.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
64	62, 63	sseldd 3922	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ Cat)
65		catciso.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
66	62, 65	sseldd 3922	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Cat)
67		f1ocnv 6728	. . . . . . . 8 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → ^◡𝐹:𝑆–1-1-onto→𝑅)
68		f1of 6716	. . . . . . . 8 ⊢ (^◡𝐹:𝑆–1-1-onto→𝑅 → ^◡𝐹:𝑆⟶𝑅)
69	1, 67, 68	3syl 18	. . . . . . 7 ⊢ (𝜑 → ^◡𝐹:𝑆⟶𝑅)
70		ovex 7308	. . . . . . . . . 10 ⊢ ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
71	70	cnvex 7772	. . . . . . . . 9 ⊢ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
72	17, 71	fnmpoi 7910	. . . . . . . 8 ⊢ 𝐻 Fn (𝑆 × 𝑆)
73	72	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
74	33	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
75	69	ffvelrnda 6961	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (^◡𝐹‘𝑢) ∈ 𝑅)
76	75	adantrr 714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑢) ∈ 𝑅)
77	69	ffvelrnda 6961	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑣) ∈ 𝑅)
78	77	adantrl 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑣) ∈ 𝑅)
79	30, 31, 32, 74, 76, 78	ffthf1o 17635	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
80		f1ocnv 6728	. . . . . . . . 9 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
81		f1of 6716	. . . . . . . . 9 ⊢ (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
82	79, 80, 81	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
83		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
84	83	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
85		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
86	85	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑣))
87	84, 86	oveq12d 7293	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
88	87	cnveqd 5784	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
89		ovex 7308	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
90	89	cnvex 7772	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
91	88, 17, 90	ovmpoa 7428	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
92	91	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
93	1	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹:𝑅–1-1-onto→𝑆)
94		simprl 768	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑢 ∈ 𝑆)
95		f1ocnvfv2 7149	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
96	93, 94, 95	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
97		simprr 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑣 ∈ 𝑆)
98		f1ocnvfv2 7149	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
99	93, 97, 98	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
100	96, 99	oveq12d 7293	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
101	100	eqcomd 2744	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢(Hom ‘𝑌)𝑣) = ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
102	92, 101	feq12d 6588	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) ↔ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))))
103	82, 102	mpbird 256	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
104		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝑆)
105		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑥 = 𝑢)
106	105	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
107		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑦 = 𝑢)
108	107	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑢))
109	106, 108	oveq12d 7293	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
110	109	cnveqd 5784	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
111		ovex 7308	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
112	111	cnvex 7772	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
113	110, 17, 112	ovmpoa 7428	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
114	104, 104, 113	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
115	114	fveq1d 6776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)))
116	51	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹(𝑋 Func 𝑌)𝐺)
117	30, 54, 53, 116, 75	funcid 17585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))))
118	1, 95	sylan 580	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
119	118	fveq2d 6778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
120	117, 119	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
121	33	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
122	30, 31, 32, 121, 75, 75	ffthf1o 17635	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑢))))
123	66	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑋 ∈ Cat)
124	30, 31, 54, 123, 75	catidcl 17391	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑋)‘(^◡𝐹‘𝑢)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢)))
125		f1ocnvfv 7150	. . . . . . . . . 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 2778	. . . . . . 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	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑢) ∈ 𝑅)
133		simp22 1206	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑣 ∈ 𝑆)
134	130, 133	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑣) ∈ 𝑅)
135		simp23 1207	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑧 ∈ 𝑆)
136	130, 135	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑧) ∈ 𝑅)
137	33	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
138	30, 31, 32, 137, 132, 134	ffthf1o 17635	. . . . . . . . . . . . . 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 7293	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
143	142	f1oeq3d 6713	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
144	138, 143	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
145		f1ocnv 6728	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
146		f1of 6716	. . . . . . . . . . . . 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	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
150	30, 31, 32, 137, 134, 136	ffthf1o 17635	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
151		f1ocnvfv2 7149	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑧 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
152	139, 135, 151	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
153	141, 152	oveq12d 7293	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑣(Hom ‘𝑌)𝑧))
154	153	f1oeq3d 6713	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) ↔ ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧)))
155	150, 154	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧))
156		f1ocnv 6728	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
157		f1of 6716	. . . . . . . . . . . . 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	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔) ∈ ((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
161	30, 31, 56, 55, 129, 132, 134, 136, 149, 160	funcco 17586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
162	140, 141	opeq12d 4812	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩ = ⟨𝑢, 𝑣⟩)
163	162, 152	oveq12d 7293	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧))
164		f1ocnvfv2 7149	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧)) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
165	155, 159, 164	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
166		f1ocnvfv2 7149	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) ∧ 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣)) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
167	144, 148, 166	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
168	163, 165, 167	oveq123d 7296	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
169	161, 168	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
170	30, 31, 32, 137, 132, 136	ffthf1o 17635	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
171	140, 152	oveq12d 7293	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑢(Hom ‘𝑌)𝑧))
172	171	f1oeq3d 6713	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧)))
173	170, 172	mpbid 231	. . . . . . . . . 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 17394	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
176		f1ocnvfv 7150	. . . . . . . . . 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 483	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑢)
180	179	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
181		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
182	181	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
183	180, 182	oveq12d 7293	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
184	183	cnveqd 5784	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
185		ovex 7308	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
186	185	cnvex 7772	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
187	184, 17, 186	ovmpoa 7428	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
188	131, 135, 187	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
189	188	fveq1d 6776	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)))
190		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑣)
191	190	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑣))
192		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
193	192	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
194	191, 193	oveq12d 7293	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
195	194	cnveqd 5784	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
196		ovex 7308	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
197	196	cnvex 7772	. . . . . . . . . . . 12 ⊢ ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
198	195, 17, 197	ovmpoa 7428	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
199	133, 135, 198	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
200	199	fveq1d 6776	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑣𝐻𝑧)‘𝑔) = (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))
201	131, 133, 91	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
202	201	fveq1d 6776	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑣)‘𝑓) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))
203	200, 202	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)))
204	178, 189, 203	3eqtr4d 2788	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)))
205	52, 30, 32, 31, 53, 54, 55, 56, 64, 66, 69, 73, 103, 128, 204	isfuncd 17580	. . . . . 6 ⊢ (𝜑 → ^◡𝐹(𝑌 Func 𝑋)𝐻)
206	30, 51, 205	cofuval2 17602	. . . . 5 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩)
207		eqid 2738	. . . . . 6 ⊢ (id_func‘𝑋) = (id_func‘𝑋)
208	207, 30, 66, 31	idfuval 17591	. . . . 5 ⊢ (𝜑 → (id_func‘𝑋) = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
209	46, 206, 208	3eqtr4d 2788	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = (id_func‘𝑋))
210		eqid 2738	. . . . 5 ⊢ (comp‘𝐶) = (comp‘𝐶)
211		df-br 5075	. . . . . 6 ⊢ (𝐹(𝑋 Func 𝑌)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
212	51, 211	sylib 217	. . . . 5 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
213		df-br 5075	. . . . . 6 ⊢ (^◡𝐹(𝑌 Func 𝑋)𝐻 ↔ ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
214	205, 213	sylib 217	. . . . 5 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
215	57, 58, 59, 210, 65, 63, 65, 212, 214	catcco 17820	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩))
216		eqid 2738	. . . . 5 ⊢ (Id‘𝐶) = (Id‘𝐶)
217	57, 58, 216, 207, 59, 65	catcid 17822	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑋) = (id_func‘𝑋))
218	209, 215, 217	3eqtr4d 2788	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋))
219		eqid 2738	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
220		eqid 2738	. . . 4 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
221	57	catccat 17823	. . . . 5 ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
222	59, 221	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
223	57, 58, 59, 219, 65, 63	catchom 17818	. . . . 5 ⊢ (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌))
224	212, 223	eleqtrrd 2842	. . . 4 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋(Hom ‘𝐶)𝑌))
225	57, 58, 59, 219, 63, 65	catchom 17818	. . . . 5 ⊢ (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋))
226	214, 225	eleqtrrd 2842	. . . 4 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌(Hom ‘𝐶)𝑋))
227	58, 219, 210, 216, 220, 222, 65, 63, 224, 226	issect2 17466	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩ ↔ (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋)))
228	218, 227	mpbird 256	. 2 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩)
229		f1ococnv2 6743	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
230	1, 229	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
231	91	3adant1 1129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
232	231	coeq2d 5771	. . . . . . . . 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 17635	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
237	100	3impb 1114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
238	237	f1oeq3d 6713	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
239	236, 238	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
240		f1ococnv2 6743	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
241	239, 240	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
242	232, 241	eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
243	242	mpoeq3dva 7352	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣))))
244		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩))
245		df-ov 7278	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑌)𝑣) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩)
246	244, 245	eqtr4di 2796	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = (𝑢(Hom ‘𝑌)𝑣))
247	246	reseq2d 5891	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑌)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
248	247	mpompt 7388	. . . . . . 7 ⊢ (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
249	243, 248	eqtr4di 2796	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))))
250	230, 249	opeq12d 4812	. . . . 5 ⊢ (𝜑 → ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩ = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
251	52, 205, 51	cofuval2 17602	. . . . 5 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩)
252		eqid 2738	. . . . . 6 ⊢ (id_func‘𝑌) = (id_func‘𝑌)
253	252, 52, 64, 32	idfuval 17591	. . . . 5 ⊢ (𝜑 → (id_func‘𝑌) = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
254	250, 251, 253	3eqtr4d 2788	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = (id_func‘𝑌))
255	57, 58, 59, 210, 63, 65, 63, 214, 212	catcco 17820	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩))
256	57, 58, 216, 252, 59, 63	catcid 17822	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑌) = (id_func‘𝑌))
257	254, 255, 256	3eqtr4d 2788	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌))
258	58, 219, 210, 216, 220, 222, 63, 65, 226, 224	issect2 17466	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩ ↔ (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌)))
259	257, 258	mpbird 256	. 2 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)
260		catcisolem.i	. . 3 ⊢ 𝐼 = (Inv‘𝐶)
261	58, 260, 222, 65, 63, 220	isinv 17472	. 2 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨^◡𝐹, 𝐻⟩ ↔ (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩ ∧ ⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)))
262	228, 259, 261	mpbir2and 710	1 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨^◡𝐹, 𝐻⟩)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∩ cin 3886 ⟨cop 4567 class class class wbr 5074 ↦ cmpt 5157 I cid 5488 × cxp 5587 ^◡ccnv 5588 ↾ cres 5591 ∘ ccom 5593 Fn wfn 6428 ⟶wf 6429 –1-1-onto→wf1o 6432 ‘cfv 6433 (class class class)co 7275 ∈ cmpo 7277 Basecbs 16912 Hom chom 16973 compcco 16974 Catccat 17373 Idccid 17374 Sectcsect 17456 Invcinv 17457 Func cfunc 17569 id_funccidfu 17570 ∘_func ccofu 17571 Full cful 17618 Faith cfth 17619 CatCatccatc 17813

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-er 8498 df-map 8617 df-ixp 8686 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-fz 13240 df-struct 16848 df-slot 16883 df-ndx 16895 df-base 16913 df-hom 16986 df-cco 16987 df-cat 17377 df-cid 17378 df-sect 17459 df-inv 17460 df-func 17573 df-idfu 17574 df-cofu 17575 df-full 17620 df-fth 17621 df-catc 17814

This theorem is referenced by: catciso 17826

W3C validator