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 17365

Description: Lemma for catciso 17366. (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 6642	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝑅))
4	1	3ad2ant1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅–1-1-onto→𝑆)
5		f1of 6614	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → 𝐹:𝑅⟶𝑆)
6	4, 5	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹:𝑅⟶𝑆)
7		simp2 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑢 ∈ 𝑅)
8	6, 7	ffvelrnd 6851	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑢) ∈ 𝑆)
9		simp3 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝑣 ∈ 𝑅)
10	6, 9	ffvelrnd 6851	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝐹‘𝑣) ∈ 𝑆)
11		simpl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑥 = (𝐹‘𝑢))
12	11	fveq2d 6673	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑥) = (^◡𝐹‘(𝐹‘𝑢)))
13		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → 𝑦 = (𝐹‘𝑣))
14	13	fveq2d 6673	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → (^◡𝐹‘𝑦) = (^◡𝐹‘(𝐹‘𝑣)))
15	12, 14	oveq12d 7173	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
16	15	cnveqd 5745	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐹‘𝑢) ∧ 𝑦 = (𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
17		catcisolem.g	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)))
18		ovex 7188	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
19	18	cnvex 7629	. . . . . . . . . . . . 13 ⊢ ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) ∈ V
20	16, 17, 19	ovmpoa 7304	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑢) ∈ 𝑆 ∧ (𝐹‘𝑣) ∈ 𝑆) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
21	8, 10, 20	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))))
22		f1ocnvfv1 7032	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
23	4, 7, 22	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑢)) = 𝑢)
24		f1ocnvfv1 7032	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
25	4, 9, 24	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡𝐹‘(𝐹‘𝑣)) = 𝑣)
26	23, 25	oveq12d 7173	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = (𝑢𝐺𝑣))
27	26	cnveqd 5745	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ^◡((^◡𝐹‘(𝐹‘𝑢))𝐺(^◡𝐹‘(𝐹‘𝑣))) = ^◡(𝑢𝐺𝑣))
28	21, 27	eqtrd 2856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → ((𝐹‘𝑢)𝐻(𝐹‘𝑣)) = ^◡(𝑢𝐺𝑣))
29	28	coeq1d 5731	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)))
30		catciso.r	. . . . . . . . . . 11 ⊢ 𝑅 = (Base‘𝑋)
31		eqid 2821	. . . . . . . . . . 11 ⊢ (Hom ‘𝑋) = (Hom ‘𝑋)
32		eqid 2821	. . . . . . . . . . 11 ⊢ (Hom ‘𝑌) = (Hom ‘𝑌)
33		catcisolem.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
34	33	3ad2ant1 1129	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
35	30, 31, 32, 34, 7, 9	ffthf1o 17188	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)))
36		f1ococnv1 6642	. . . . . . . . . 10 ⊢ ((𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹‘𝑢)(Hom ‘𝑌)(𝐹‘𝑣)) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
37	35, 36	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (^◡(𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
38	29, 37	eqtrd 2856	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅) → (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
39	38	mpoeq3dva 7230	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣))))
40		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩))
41		df-ov 7158	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑋)𝑣) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩)
42	40, 41	syl6eqr 2874	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = (𝑢(Hom ‘𝑋)𝑣))
43	42	reseq2d 5852	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑋)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
44	43	mpompt 7265	. . . . . . 7 ⊢ (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))) = (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
45	39, 44	syl6eqr 2874	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))))
46	3, 45	opeq12d 4810	. . . . 5 ⊢ (𝜑 → ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩ = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
47		inss1 4204	. . . . . . . . 9 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Full 𝑌)
48		fullfunc 17175	. . . . . . . . 9 ⊢ (𝑋 Full 𝑌) ⊆ (𝑋 Func 𝑌)
49	47, 48	sstri 3975	. . . . . . . 8 ⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Func 𝑌)
50	49	ssbri 5110	. . . . . . 7 ⊢ (𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺 → 𝐹(𝑋 Func 𝑌)𝐺)
51	33, 50	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹(𝑋 Func 𝑌)𝐺)
52		catciso.s	. . . . . . 7 ⊢ 𝑆 = (Base‘𝑌)
53		eqid 2821	. . . . . . 7 ⊢ (Id‘𝑌) = (Id‘𝑌)
54		eqid 2821	. . . . . . 7 ⊢ (Id‘𝑋) = (Id‘𝑋)
55		eqid 2821	. . . . . . 7 ⊢ (comp‘𝑌) = (comp‘𝑌)
56		eqid 2821	. . . . . . 7 ⊢ (comp‘𝑋) = (comp‘𝑋)
57		catciso.c	. . . . . . . . . 10 ⊢ 𝐶 = (CatCat‘𝑈)
58		catciso.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
59		catciso.u	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
60	57, 58, 59	catcbas 17356	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
61		inss2 4205	. . . . . . . . 9 ⊢ (𝑈 ∩ Cat) ⊆ Cat
62	60, 61	eqsstrdi 4020	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ Cat)
63		catciso.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
64	62, 63	sseldd 3967	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ Cat)
65		catciso.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
66	62, 65	sseldd 3967	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Cat)
67		f1ocnv 6626	. . . . . . . 8 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → ^◡𝐹:𝑆–1-1-onto→𝑅)
68		f1of 6614	. . . . . . . 8 ⊢ (^◡𝐹:𝑆–1-1-onto→𝑅 → ^◡𝐹:𝑆⟶𝑅)
69	1, 67, 68	3syl 18	. . . . . . 7 ⊢ (𝜑 → ^◡𝐹:𝑆⟶𝑅)
70		ovex 7188	. . . . . . . . . 10 ⊢ ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
71	70	cnvex 7629	. . . . . . . . 9 ⊢ ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) ∈ V
72	17, 71	fnmpoi 7767	. . . . . . . 8 ⊢ 𝐻 Fn (𝑆 × 𝑆)
73	72	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
74	33	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
75	69	ffvelrnda 6850	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (^◡𝐹‘𝑢) ∈ 𝑅)
76	75	adantrr 715	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑢) ∈ 𝑅)
77	69	ffvelrnda 6850	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑣) ∈ 𝑅)
78	77	adantrl 714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (^◡𝐹‘𝑣) ∈ 𝑅)
79	30, 31, 32, 74, 76, 78	ffthf1o 17188	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
80		f1ocnv 6626	. . . . . . . . 9 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
81		f1of 6614	. . . . . . . . 9 ⊢ (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
82	79, 80, 81	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
83		simpl 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
84	83	fveq2d 6673	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
85		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
86	85	fveq2d 6673	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑣))
87	84, 86	oveq12d 7173	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
88	87	cnveqd 5745	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
89		ovex 7188	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
90	89	cnvex 7629	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∈ V
91	88, 17, 90	ovmpoa 7304	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
92	91	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
93	1	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝐹:𝑅–1-1-onto→𝑆)
94		simprl 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑢 ∈ 𝑆)
95		f1ocnvfv2 7033	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
96	93, 94, 95	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
97		simprr 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑣 ∈ 𝑆)
98		f1ocnvfv2 7033	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑣 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
99	93, 97, 98	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
100	96, 99	oveq12d 7173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
101	100	eqcomd 2827	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢(Hom ‘𝑌)𝑣) = ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
102	92, 101	feq12d 6501	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) ↔ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣)))⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))))
103	82, 102	mpbird 259	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
104		simpr 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝑆)
105		simpl 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑥 = 𝑢)
106	105	fveq2d 6673	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
107		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑦 = 𝑢)
108	107	fveq2d 6673	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑢))
109	106, 108	oveq12d 7173	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
110	109	cnveqd 5745	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
111		ovex 7188	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
112	111	cnvex 7629	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)) ∈ V
113	110, 17, 112	ovmpoa 7304	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
114	104, 104, 113	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝑢𝐻𝑢) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)))
115	114	fveq1d 6671	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)))
116	51	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹(𝑋 Func 𝑌)𝐺)
117	30, 54, 53, 116, 75	funcid 17139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))))
118	1, 95	sylan 582	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
119	118	fveq2d 6673	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑌)‘(𝐹‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
120	117, 119	eqtrd 2856	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢))
121	33	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
122	30, 31, 32, 121, 75, 75	ffthf1o 17188	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑢))))
123	66	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑋 ∈ Cat)
124	30, 31, 54, 123, 75	catidcl 16952	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((Id‘𝑋)‘(^◡𝐹‘𝑢)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢)))
125		f1ocnvfv 7034	. . . . . . . . . 10 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑢))) ∧ ((Id‘𝑋)‘(^◡𝐹‘𝑢)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑢))) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢))))
126	122, 124, 125	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑋)‘(^◡𝐹‘𝑢))) = ((Id‘𝑌)‘𝑢) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢))))
127	120, 126	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢)))
128	115, 127	eqtrd 2856	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(^◡𝐹‘𝑢)))
129	51	3ad2ant1 1129	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹(𝑋 Func 𝑌)𝐺)
130	69	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡𝐹:𝑆⟶𝑅)
131		simp21 1202	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑢 ∈ 𝑆)
132	130, 131	ffvelrnd 6851	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑢) ∈ 𝑅)
133		simp22 1203	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑣 ∈ 𝑆)
134	130, 133	ffvelrnd 6851	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑣) ∈ 𝑅)
135		simp23 1204	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑧 ∈ 𝑆)
136	130, 135	ffvelrnd 6851	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡𝐹‘𝑧) ∈ 𝑅)
137	33	3ad2ant1 1129	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
138	30, 31, 32, 137, 132, 134	ffthf1o 17188	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
139	1	3ad2ant1 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹:𝑅–1-1-onto→𝑆)
140	139, 131, 95	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑢)) = 𝑢)
141	139, 133, 98	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑣)) = 𝑣)
142	140, 141	oveq12d 7173	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
143	142	f1oeq3d 6611	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
144	138, 143	mpbid 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
145		f1ocnv 6626	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
146		f1of 6614	. . . . . . . . . . . . 13 ⊢ (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
147	144, 145, 146	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
148		simp3l 1197	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣))
149	147, 148	ffvelrnd 6851	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣)))
150	30, 31, 32, 137, 134, 136	ffthf1o 17188	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
151		f1ocnvfv2 7033	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝑅–1-1-onto→𝑆 ∧ 𝑧 ∈ 𝑆) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
152	139, 135, 151	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
153	141, 152	oveq12d 7173	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑣(Hom ‘𝑌)𝑧))
154	153	f1oeq3d 6611	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑣))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) ↔ ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧)))
155	150, 154	mpbid 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧))
156		f1ocnv 6626	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
157		f1of 6614	. . . . . . . . . . . . 13 ⊢ (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
158	155, 156, 157	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
159		simp3r 1198	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))
160	158, 159	ffvelrnd 6851	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔) ∈ ((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
161	30, 31, 56, 55, 129, 132, 134, 136, 149, 160	funcco 17140	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
162	140, 141	opeq12d 4810	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩ = ⟨𝑢, 𝑣⟩)
163	162, 152	oveq12d 7173	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧))
164		f1ocnvfv2 7033	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑣)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧)) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
165	155, 159, 164	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)) = 𝑔)
166		f1ocnvfv2 7033	. . . . . . . . . . . 12 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) ∧ 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣)) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
167	144, 148, 166	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) = 𝑓)
168	163, 165, 167	oveq123d 7176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘(^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))(⟨(𝐹‘(^◡𝐹‘𝑢)), (𝐹‘(^◡𝐹‘𝑣))⟩(comp‘𝑌)(𝐹‘(^◡𝐹‘𝑧)))(((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
169	161, 168	eqtrd 2856	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
170	30, 31, 32, 137, 132, 136	ffthf1o 17188	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))))
171	140, 152	oveq12d 7173	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) = (𝑢(Hom ‘𝑌)𝑧))
172	171	f1oeq3d 6611	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑧))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧)))
173	170, 172	mpbid 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧))
174	66	3ad2ant1 1129	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑋 ∈ Cat)
175	30, 31, 56, 174, 132, 134, 136, 149, 160	catcocl 16955	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧)))
176		f1ocnvfv 7034	. . . . . . . . . 10 ⊢ ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧) ∧ ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)) ∈ ((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑧))) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
177	173, 175, 176	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))))
178	169, 177	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)))
179		simpl 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑢)
180	179	fveq2d 6673	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑢))
181		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
182	181	fveq2d 6673	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
183	180, 182	oveq12d 7173	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
184	183	cnveqd 5745	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
185		ovex 7188	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
186	185	cnvex 7629	. . . . . . . . . . 11 ⊢ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)) ∈ V
187	184, 17, 186	ovmpoa 7304	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
188	131, 135, 187	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑧) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧)))
189	188	fveq1d 6671	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)))
190		simpl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑣)
191	190	fveq2d 6673	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑥) = (^◡𝐹‘𝑣))
192		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
193	192	fveq2d 6673	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → (^◡𝐹‘𝑦) = (^◡𝐹‘𝑧))
194	191, 193	oveq12d 7173	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
195	194	cnveqd 5745	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑧) → ^◡((^◡𝐹‘𝑥)𝐺(^◡𝐹‘𝑦)) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
196		ovex 7188	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
197	196	cnvex 7629	. . . . . . . . . . . 12 ⊢ ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)) ∈ V
198	195, 17, 197	ovmpoa 7304	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
199	133, 135, 198	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑣𝐻𝑧) = ^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧)))
200	199	fveq1d 6671	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑣𝐻𝑧)‘𝑔) = (^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔))
201	131, 133, 91	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
202	201	fveq1d 6671	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑣)‘𝑓) = (^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓))
203	200, 202	oveq12d 7173	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)) = ((^◡((^◡𝐹‘𝑣)𝐺(^◡𝐹‘𝑧))‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))(^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))‘𝑓)))
204	178, 189, 203	3eqtr4d 2866	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (((𝑣𝐻𝑧)‘𝑔)(⟨(^◡𝐹‘𝑢), (^◡𝐹‘𝑣)⟩(comp‘𝑋)(^◡𝐹‘𝑧))((𝑢𝐻𝑣)‘𝑓)))
205	52, 30, 32, 31, 53, 54, 55, 56, 64, 66, 69, 73, 103, 128, 204	isfuncd 17134	. . . . . 6 ⊢ (𝜑 → ^◡𝐹(𝑌 Func 𝑋)𝐻)
206	30, 51, 205	cofuval2 17156	. . . . 5 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = ⟨(^◡𝐹 ∘ 𝐹), (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑅 ↦ (((𝐹‘𝑢)𝐻(𝐹‘𝑣)) ∘ (𝑢𝐺𝑣)))⟩)
207		eqid 2821	. . . . . 6 ⊢ (id_func‘𝑋) = (id_func‘𝑋)
208	207, 30, 66, 31	idfuval 17145	. . . . 5 ⊢ (𝜑 → (id_func‘𝑋) = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
209	46, 206, 208	3eqtr4d 2866	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩) = (id_func‘𝑋))
210		eqid 2821	. . . . 5 ⊢ (comp‘𝐶) = (comp‘𝐶)
211		df-br 5066	. . . . . 6 ⊢ (𝐹(𝑋 Func 𝑌)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
212	51, 211	sylib 220	. . . . 5 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
213		df-br 5066	. . . . . 6 ⊢ (^◡𝐹(𝑌 Func 𝑋)𝐻 ↔ ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
214	205, 213	sylib 220	. . . . 5 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
215	57, 58, 59, 210, 65, 63, 65, 212, 214	catcco 17360	. . . 4 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = (⟨^◡𝐹, 𝐻⟩ ∘_func ⟨𝐹, 𝐺⟩))
216		eqid 2821	. . . . 5 ⊢ (Id‘𝐶) = (Id‘𝐶)
217	57, 58, 216, 207, 59, 65	catcid 17362	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑋) = (id_func‘𝑋))
218	209, 215, 217	3eqtr4d 2866	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋))
219		eqid 2821	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
220		eqid 2821	. . . 4 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
221	57	catccat 17363	. . . . 5 ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
222	59, 221	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
223	57, 58, 59, 219, 65, 63	catchom 17358	. . . . 5 ⊢ (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌))
224	212, 223	eleqtrrd 2916	. . . 4 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋(Hom ‘𝐶)𝑌))
225	57, 58, 59, 219, 63, 65	catchom 17358	. . . . 5 ⊢ (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋))
226	214, 225	eleqtrrd 2916	. . . 4 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩ ∈ (𝑌(Hom ‘𝐶)𝑋))
227	58, 219, 210, 216, 220, 222, 65, 63, 224, 226	issect2 17023	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩ ↔ (⟨^◡𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋)))
228	218, 227	mpbird 259	. 2 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩)
229		f1ococnv2 6640	. . . . . . 7 ⊢ (𝐹:𝑅–1-1-onto→𝑆 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
230	1, 229	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘ ^◡𝐹) = ( I ↾ 𝑆))
231	91	3adant1 1126	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢𝐻𝑣) = ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)))
232	231	coeq2d 5732	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)) = (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))))
233	33	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
234	75	3adant3 1128	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑢) ∈ 𝑅)
235	77	3adant2 1127	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (^◡𝐹‘𝑣) ∈ 𝑅)
236	30, 31, 32, 233, 234, 235	ffthf1o 17188	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))))
237	100	3impb 1111	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
238	237	f1oeq3d 6611	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→((𝐹‘(^◡𝐹‘𝑢))(Hom ‘𝑌)(𝐹‘(^◡𝐹‘𝑣))) ↔ ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
239	236, 238	mpbid 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
240		f1ococnv2 6640	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)):((^◡𝐹‘𝑢)(Hom ‘𝑋)(^◡𝐹‘𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
241	239, 240	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ ^◡((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
242	232, 241	eqtrd 2856	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
243	242	mpoeq3dva 7230	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣))))
244		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩))
245		df-ov 7158	. . . . . . . . . 10 ⊢ (𝑢(Hom ‘𝑌)𝑣) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩)
246	244, 245	syl6eqr 2874	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = (𝑢(Hom ‘𝑌)𝑣))
247	246	reseq2d 5852	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑌)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
248	247	mpompt 7265	. . . . . . 7 ⊢ (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))) = (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
249	243, 248	syl6eqr 2874	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))))
250	230, 249	opeq12d 4810	. . . . 5 ⊢ (𝜑 → ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩ = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
251	52, 205, 51	cofuval2 17156	. . . . 5 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = ⟨(𝐹 ∘ ^◡𝐹), (𝑢 ∈ 𝑆, 𝑣 ∈ 𝑆 ↦ (((^◡𝐹‘𝑢)𝐺(^◡𝐹‘𝑣)) ∘ (𝑢𝐻𝑣)))⟩)
252		eqid 2821	. . . . . 6 ⊢ (id_func‘𝑌) = (id_func‘𝑌)
253	252, 52, 64, 32	idfuval 17145	. . . . 5 ⊢ (𝜑 → (id_func‘𝑌) = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
254	250, 251, 253	3eqtr4d 2866	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩) = (id_func‘𝑌))
255	57, 58, 59, 210, 63, 65, 63, 214, 212	catcco 17360	. . . 4 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = (⟨𝐹, 𝐺⟩ ∘_func ⟨^◡𝐹, 𝐻⟩))
256	57, 58, 216, 252, 59, 63	catcid 17362	. . . 4 ⊢ (𝜑 → ((Id‘𝐶)‘𝑌) = (id_func‘𝑌))
257	254, 255, 256	3eqtr4d 2866	. . 3 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌))
258	58, 219, 210, 216, 220, 222, 63, 65, 226, 224	issect2 17023	. . 3 ⊢ (𝜑 → (⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩ ↔ (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌)))
259	257, 258	mpbird 259	. 2 ⊢ (𝜑 → ⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)
260		catcisolem.i	. . 3 ⊢ 𝐼 = (Inv‘𝐶)
261	58, 260, 222, 65, 63, 220	isinv 17029	. 2 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨^◡𝐹, 𝐻⟩ ↔ (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨^◡𝐹, 𝐻⟩ ∧ ⟨^◡𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)))
262	228, 259, 261	mpbir2and 711	1 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨^◡𝐹, 𝐻⟩)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∩ cin 3934 ⟨cop 4572 class class class wbr 5065 ↦ cmpt 5145 I cid 5458 × cxp 5552 ^◡ccnv 5553 ↾ cres 5556 ∘ ccom 5558 Fn wfn 6349 ⟶wf 6350 –1-1-onto→wf1o 6353 ‘cfv 6354 (class class class)co 7155 ∈ cmpo 7157 Basecbs 16482 Hom chom 16575 compcco 16576 Catccat 16934 Idccid 16935 Sectcsect 17013 Invcinv 17014 Func cfunc 17123 id_funccidfu 17124 ∘_func ccofu 17125 Full cful 17171 Faith cfth 17172 CatCatccatc 17353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5189 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460 ax-cnex 10592 ax-resscn 10593 ax-1cn 10594 ax-icn 10595 ax-addcl 10596 ax-addrcl 10597 ax-mulcl 10598 ax-mulrcl 10599 ax-mulcom 10600 ax-addass 10601 ax-mulass 10602 ax-distr 10603 ax-i2m1 10604 ax-1ne0 10605 ax-1rid 10606 ax-rnegex 10607 ax-rrecex 10608 ax-cnre 10609 ax-pre-lttri 10610 ax-pre-lttrn 10611 ax-pre-ltadd 10612 ax-pre-mulgt0 10613

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-int 4876 df-iun 4920 df-br 5066 df-opab 5128 df-mpt 5146 df-tr 5172 df-id 5459 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-we 5515 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-rn 5565 df-res 5566 df-ima 5567 df-pred 6147 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 df-iota 6313 df-fun 6356 df-fn 6357 df-f 6358 df-f1 6359 df-fo 6360 df-f1o 6361 df-fv 6362 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-om 7580 df-1st 7688 df-2nd 7689 df-wrecs 7946 df-recs 8007 df-rdg 8045 df-1o 8101 df-oadd 8105 df-er 8288 df-map 8407 df-ixp 8461 df-en 8509 df-dom 8510 df-sdom 8511 df-fin 8512 df-pnf 10676 df-mnf 10677 df-xr 10678 df-ltxr 10679 df-le 10680 df-sub 10871 df-neg 10872 df-nn 11638 df-2 11699 df-3 11700 df-4 11701 df-5 11702 df-6 11703 df-7 11704 df-8 11705 df-9 11706 df-n0 11897 df-z 11981 df-dec 12098 df-uz 12243 df-fz 12892 df-struct 16484 df-ndx 16485 df-slot 16486 df-base 16488 df-hom 16588 df-cco 16589 df-cat 16938 df-cid 16939 df-sect 17016 df-inv 17017 df-func 17127 df-idfu 17128 df-cofu 17129 df-full 17173 df-fth 17174 df-catc 17354

This theorem is referenced by: catciso 17366

W3C validator