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

Theorem catcisolem 16525
Description: Lemma for catciso 16526. (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.
StepHypRef Expression
1 catcisolem.2 . . . . . . 7 (𝜑𝐹:𝑅1-1-onto𝑆)
2 f1ococnv1 6063 . . . . . . 7 (𝐹:𝑅1-1-onto𝑆 → (𝐹𝐹) = ( I ↾ 𝑅))
31, 2syl 17 . . . . . 6 (𝜑 → (𝐹𝐹) = ( I ↾ 𝑅))
413ad2ant1 1074 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑅𝑣𝑅) → 𝐹:𝑅1-1-onto𝑆)
5 f1of 6035 . . . . . . . . . . . . . 14 (𝐹:𝑅1-1-onto𝑆𝐹:𝑅𝑆)
64, 5syl 17 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → 𝐹:𝑅𝑆)
7 simp2 1054 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → 𝑢𝑅)
86, 7ffvelrnd 6253 . . . . . . . . . . . 12 ((𝜑𝑢𝑅𝑣𝑅) → (𝐹𝑢) ∈ 𝑆)
9 simp3 1055 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → 𝑣𝑅)
106, 9ffvelrnd 6253 . . . . . . . . . . . 12 ((𝜑𝑢𝑅𝑣𝑅) → (𝐹𝑣) ∈ 𝑆)
11 simpl 471 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → 𝑥 = (𝐹𝑢))
1211fveq2d 6092 . . . . . . . . . . . . . . 15 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → (𝐹𝑥) = (𝐹‘(𝐹𝑢)))
13 simpr 475 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → 𝑦 = (𝐹𝑣))
1413fveq2d 6092 . . . . . . . . . . . . . . 15 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → (𝐹𝑦) = (𝐹‘(𝐹𝑣)))
1512, 14oveq12d 6545 . . . . . . . . . . . . . 14 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))))
1615cnveqd 5208 . . . . . . . . . . . . 13 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))))
17 catcisolem.g . . . . . . . . . . . . 13 𝐻 = (𝑥𝑆, 𝑦𝑆((𝐹𝑥)𝐺(𝐹𝑦)))
18 ovex 6555 . . . . . . . . . . . . . 14 ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))) ∈ V
1918cnvex 6983 . . . . . . . . . . . . 13 ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))) ∈ V
2016, 17, 19ovmpt2a 6667 . . . . . . . . . . . 12 (((𝐹𝑢) ∈ 𝑆 ∧ (𝐹𝑣) ∈ 𝑆) → ((𝐹𝑢)𝐻(𝐹𝑣)) = ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))))
218, 10, 20syl2anc 690 . . . . . . . . . . 11 ((𝜑𝑢𝑅𝑣𝑅) → ((𝐹𝑢)𝐻(𝐹𝑣)) = ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))))
22 f1ocnvfv1 6410 . . . . . . . . . . . . . 14 ((𝐹:𝑅1-1-onto𝑆𝑢𝑅) → (𝐹‘(𝐹𝑢)) = 𝑢)
234, 7, 22syl2anc 690 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → (𝐹‘(𝐹𝑢)) = 𝑢)
24 f1ocnvfv1 6410 . . . . . . . . . . . . . 14 ((𝐹:𝑅1-1-onto𝑆𝑣𝑅) → (𝐹‘(𝐹𝑣)) = 𝑣)
254, 9, 24syl2anc 690 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → (𝐹‘(𝐹𝑣)) = 𝑣)
2623, 25oveq12d 6545 . . . . . . . . . . . 12 ((𝜑𝑢𝑅𝑣𝑅) → ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))) = (𝑢𝐺𝑣))
2726cnveqd 5208 . . . . . . . . . . 11 ((𝜑𝑢𝑅𝑣𝑅) → ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))) = (𝑢𝐺𝑣))
2821, 27eqtrd 2643 . . . . . . . . . 10 ((𝜑𝑢𝑅𝑣𝑅) → ((𝐹𝑢)𝐻(𝐹𝑣)) = (𝑢𝐺𝑣))
2928coeq1d 5193 . . . . . . . . 9 ((𝜑𝑢𝑅𝑣𝑅) → (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣)) = ((𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)))
30 catciso.r . . . . . . . . . . 11 𝑅 = (Base‘𝑋)
31 eqid 2609 . . . . . . . . . . 11 (Hom ‘𝑋) = (Hom ‘𝑋)
32 eqid 2609 . . . . . . . . . . 11 (Hom ‘𝑌) = (Hom ‘𝑌)
33 catcisolem.1 . . . . . . . . . . . 12 (𝜑𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
34333ad2ant1 1074 . . . . . . . . . . 11 ((𝜑𝑢𝑅𝑣𝑅) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
3530, 31, 32, 34, 7, 9ffthf1o 16348 . . . . . . . . . 10 ((𝜑𝑢𝑅𝑣𝑅) → (𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹𝑢)(Hom ‘𝑌)(𝐹𝑣)))
36 f1ococnv1 6063 . . . . . . . . . 10 ((𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹𝑢)(Hom ‘𝑌)(𝐹𝑣)) → ((𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
3735, 36syl 17 . . . . . . . . 9 ((𝜑𝑢𝑅𝑣𝑅) → ((𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
3829, 37eqtrd 2643 . . . . . . . 8 ((𝜑𝑢𝑅𝑣𝑅) → (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
3938mpt2eq3dva 6595 . . . . . . 7 (𝜑 → (𝑢𝑅, 𝑣𝑅 ↦ (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑢𝑅, 𝑣𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣))))
40 fveq2 6088 . . . . . . . . . 10 (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩))
41 df-ov 6530 . . . . . . . . . 10 (𝑢(Hom ‘𝑋)𝑣) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩)
4240, 41syl6eqr 2661 . . . . . . . . 9 (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = (𝑢(Hom ‘𝑋)𝑣))
4342reseq2d 5304 . . . . . . . 8 (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑋)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
4443mpt2mpt 6628 . . . . . . 7 (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))) = (𝑢𝑅, 𝑣𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
4539, 44syl6eqr 2661 . . . . . 6 (𝜑 → (𝑢𝑅, 𝑣𝑅 ↦ (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))))
463, 45opeq12d 4342 . . . . 5 (𝜑 → ⟨(𝐹𝐹), (𝑢𝑅, 𝑣𝑅 ↦ (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣)))⟩ = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
47 inss1 3794 . . . . . . . . 9 ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Full 𝑌)
48 fullfunc 16335 . . . . . . . . 9 (𝑋 Full 𝑌) ⊆ (𝑋 Func 𝑌)
4947, 48sstri 3576 . . . . . . . 8 ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Func 𝑌)
5049ssbri 4621 . . . . . . 7 (𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺𝐹(𝑋 Func 𝑌)𝐺)
5133, 50syl 17 . . . . . 6 (𝜑𝐹(𝑋 Func 𝑌)𝐺)
52 catciso.s . . . . . . 7 𝑆 = (Base‘𝑌)
53 eqid 2609 . . . . . . 7 (Id‘𝑌) = (Id‘𝑌)
54 eqid 2609 . . . . . . 7 (Id‘𝑋) = (Id‘𝑋)
55 eqid 2609 . . . . . . 7 (comp‘𝑌) = (comp‘𝑌)
56 eqid 2609 . . . . . . 7 (comp‘𝑋) = (comp‘𝑋)
57 catciso.c . . . . . . . . . 10 𝐶 = (CatCat‘𝑈)
58 catciso.b . . . . . . . . . 10 𝐵 = (Base‘𝐶)
59 catciso.u . . . . . . . . . 10 (𝜑𝑈𝑉)
6057, 58, 59catcbas 16516 . . . . . . . . 9 (𝜑𝐵 = (𝑈 ∩ Cat))
61 inss2 3795 . . . . . . . . 9 (𝑈 ∩ Cat) ⊆ Cat
6260, 61syl6eqss 3617 . . . . . . . 8 (𝜑𝐵 ⊆ Cat)
63 catciso.y . . . . . . . 8 (𝜑𝑌𝐵)
6462, 63sseldd 3568 . . . . . . 7 (𝜑𝑌 ∈ Cat)
65 catciso.x . . . . . . . 8 (𝜑𝑋𝐵)
6662, 65sseldd 3568 . . . . . . 7 (𝜑𝑋 ∈ Cat)
67 f1ocnv 6047 . . . . . . . 8 (𝐹:𝑅1-1-onto𝑆𝐹:𝑆1-1-onto𝑅)
68 f1of 6035 . . . . . . . 8 (𝐹:𝑆1-1-onto𝑅𝐹:𝑆𝑅)
691, 67, 683syl 18 . . . . . . 7 (𝜑𝐹:𝑆𝑅)
70 ovex 6555 . . . . . . . . . 10 ((𝐹𝑥)𝐺(𝐹𝑦)) ∈ V
7170cnvex 6983 . . . . . . . . 9 ((𝐹𝑥)𝐺(𝐹𝑦)) ∈ V
7217, 71fnmpt2i 7105 . . . . . . . 8 𝐻 Fn (𝑆 × 𝑆)
7372a1i 11 . . . . . . 7 (𝜑𝐻 Fn (𝑆 × 𝑆))
7433adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
7569ffvelrnda 6252 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → (𝐹𝑢) ∈ 𝑅)
7675adantrr 748 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝐹𝑢) ∈ 𝑅)
7769ffvelrnda 6252 . . . . . . . . . . 11 ((𝜑𝑣𝑆) → (𝐹𝑣) ∈ 𝑅)
7877adantrl 747 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝐹𝑣) ∈ 𝑅)
7930, 31, 32, 74, 76, 78ffthf1o 16348 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))))
80 f1ocnv 6047 . . . . . . . . 9 (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))–1-1-onto→((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
81 f1of 6035 . . . . . . . . 9 (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))–1-1-onto→((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
8279, 80, 813syl 18 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
83 simpl 471 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
8483fveq2d 6092 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐹𝑥) = (𝐹𝑢))
85 simpr 475 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
8685fveq2d 6092 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐹𝑦) = (𝐹𝑣))
8784, 86oveq12d 6545 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑣)))
8887cnveqd 5208 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑣)))
89 ovex 6555 . . . . . . . . . . . 12 ((𝐹𝑢)𝐺(𝐹𝑣)) ∈ V
9089cnvex 6983 . . . . . . . . . . 11 ((𝐹𝑢)𝐺(𝐹𝑣)) ∈ V
9188, 17, 90ovmpt2a 6667 . . . . . . . . . 10 ((𝑢𝑆𝑣𝑆) → (𝑢𝐻𝑣) = ((𝐹𝑢)𝐺(𝐹𝑣)))
9291adantl 480 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝑢𝐻𝑣) = ((𝐹𝑢)𝐺(𝐹𝑣)))
931adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → 𝐹:𝑅1-1-onto𝑆)
94 simprl 789 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → 𝑢𝑆)
95 f1ocnvfv2 6411 . . . . . . . . . . . 12 ((𝐹:𝑅1-1-onto𝑆𝑢𝑆) → (𝐹‘(𝐹𝑢)) = 𝑢)
9693, 94, 95syl2anc 690 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝐹‘(𝐹𝑢)) = 𝑢)
97 simprr 791 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → 𝑣𝑆)
98 f1ocnvfv2 6411 . . . . . . . . . . . 12 ((𝐹:𝑅1-1-onto𝑆𝑣𝑆) → (𝐹‘(𝐹𝑣)) = 𝑣)
9993, 97, 98syl2anc 690 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝐹‘(𝐹𝑣)) = 𝑣)
10096, 99oveq12d 6545 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
101100eqcomd 2615 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝑢(Hom ‘𝑌)𝑣) = ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))))
10292, 101feq12d 5932 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → ((𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)) ↔ ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))))
10382, 102mpbird 245 . . . . . . 7 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
104 simpr 475 . . . . . . . . . 10 ((𝜑𝑢𝑆) → 𝑢𝑆)
105 simpl 471 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑢) → 𝑥 = 𝑢)
106105fveq2d 6092 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑢) → (𝐹𝑥) = (𝐹𝑢))
107 simpr 475 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑢) → 𝑦 = 𝑢)
108107fveq2d 6092 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑢) → (𝐹𝑦) = (𝐹𝑢))
109106, 108oveq12d 6545 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑢) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑢)))
110109cnveqd 5208 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑢) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑢)))
111 ovex 6555 . . . . . . . . . . . 12 ((𝐹𝑢)𝐺(𝐹𝑢)) ∈ V
112111cnvex 6983 . . . . . . . . . . 11 ((𝐹𝑢)𝐺(𝐹𝑢)) ∈ V
113110, 17, 112ovmpt2a 6667 . . . . . . . . . 10 ((𝑢𝑆𝑢𝑆) → (𝑢𝐻𝑢) = ((𝐹𝑢)𝐺(𝐹𝑢)))
114104, 104, 113syl2anc 690 . . . . . . . . 9 ((𝜑𝑢𝑆) → (𝑢𝐻𝑢) = ((𝐹𝑢)𝐺(𝐹𝑢)))
115114fveq1d 6090 . . . . . . . 8 ((𝜑𝑢𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑌)‘𝑢)))
11651adantr 479 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → 𝐹(𝑋 Func 𝑌)𝐺)
11730, 54, 53, 116, 75funcid 16299 . . . . . . . . . 10 ((𝜑𝑢𝑆) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑋)‘(𝐹𝑢))) = ((Id‘𝑌)‘(𝐹‘(𝐹𝑢))))
1181, 95sylan 486 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → (𝐹‘(𝐹𝑢)) = 𝑢)
119118fveq2d 6092 . . . . . . . . . 10 ((𝜑𝑢𝑆) → ((Id‘𝑌)‘(𝐹‘(𝐹𝑢))) = ((Id‘𝑌)‘𝑢))
120117, 119eqtrd 2643 . . . . . . . . 9 ((𝜑𝑢𝑆) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑋)‘(𝐹𝑢))) = ((Id‘𝑌)‘𝑢))
12133adantr 479 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
12230, 31, 32, 121, 75, 75ffthf1o 16348 . . . . . . . . . 10 ((𝜑𝑢𝑆) → ((𝐹𝑢)𝐺(𝐹𝑢)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑢))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑢))))
12366adantr 479 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → 𝑋 ∈ Cat)
12430, 31, 54, 123, 75catidcl 16112 . . . . . . . . . 10 ((𝜑𝑢𝑆) → ((Id‘𝑋)‘(𝐹𝑢)) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑢)))
125 f1ocnvfv 6412 . . . . . . . . . 10 ((((𝐹𝑢)𝐺(𝐹𝑢)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑢))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑢))) ∧ ((Id‘𝑋)‘(𝐹𝑢)) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑢))) → ((((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑋)‘(𝐹𝑢))) = ((Id‘𝑌)‘𝑢) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(𝐹𝑢))))
126122, 124, 125syl2anc 690 . . . . . . . . 9 ((𝜑𝑢𝑆) → ((((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑋)‘(𝐹𝑢))) = ((Id‘𝑌)‘𝑢) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(𝐹𝑢))))
127120, 126mpd 15 . . . . . . . 8 ((𝜑𝑢𝑆) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(𝐹𝑢)))
128115, 127eqtrd 2643 . . . . . . 7 ((𝜑𝑢𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(𝐹𝑢)))
129513ad2ant1 1074 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹(𝑋 Func 𝑌)𝐺)
130693ad2ant1 1074 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹:𝑆𝑅)
131 simp21 1086 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑢𝑆)
132130, 131ffvelrnd 6253 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹𝑢) ∈ 𝑅)
133 simp22 1087 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑣𝑆)
134130, 133ffvelrnd 6253 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹𝑣) ∈ 𝑅)
135 simp23 1088 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑧𝑆)
136130, 135ffvelrnd 6253 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹𝑧) ∈ 𝑅)
137333ad2ant1 1074 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
13830, 31, 32, 137, 132, 134ffthf1o 16348 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))))
13913ad2ant1 1074 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹:𝑅1-1-onto𝑆)
140139, 131, 95syl2anc 690 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(𝐹𝑢)) = 𝑢)
141139, 133, 98syl2anc 690 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(𝐹𝑣)) = 𝑣)
142140, 141oveq12d 6545 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
143 f1oeq3 6027 . . . . . . . . . . . . . . 15 (((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) = (𝑢(Hom ‘𝑌)𝑣) → (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) ↔ ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
144142, 143syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) ↔ ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
145138, 144mpbid 220 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
146 f1ocnv 6047 . . . . . . . . . . . . 13 (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → ((𝐹𝑢)𝐺(𝐹𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
147 f1of 6035 . . . . . . . . . . . . 13 (((𝐹𝑢)𝐺(𝐹𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)) → ((𝐹𝑢)𝐺(𝐹𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
148145, 146, 1473syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
149 simp3l 1081 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣))
150148, 149ffvelrnd 6253 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
15130, 31, 32, 137, 134, 136ffthf1o 16348 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→((𝐹‘(𝐹𝑣))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))))
152 f1ocnvfv2 6411 . . . . . . . . . . . . . . . . 17 ((𝐹:𝑅1-1-onto𝑆𝑧𝑆) → (𝐹‘(𝐹𝑧)) = 𝑧)
153139, 135, 152syl2anc 690 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(𝐹𝑧)) = 𝑧)
154141, 153oveq12d 6545 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(𝐹𝑣))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) = (𝑣(Hom ‘𝑌)𝑧))
155 f1oeq3 6027 . . . . . . . . . . . . . . 15 (((𝐹‘(𝐹𝑣))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) = (𝑣(Hom ‘𝑌)𝑧) → (((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→((𝐹‘(𝐹𝑣))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) ↔ ((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧)))
156154, 155syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→((𝐹‘(𝐹𝑣))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) ↔ ((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧)))
157151, 156mpbid 220 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧))
158 f1ocnv 6047 . . . . . . . . . . . . 13 (((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) → ((𝐹𝑣)𝐺(𝐹𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)))
159 f1of 6035 . . . . . . . . . . . . 13 (((𝐹𝑣)𝐺(𝐹𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)) → ((𝐹𝑣)𝐺(𝐹𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)))
160157, 158, 1593syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑣)𝐺(𝐹𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)))
161 simp3r 1082 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))
162160, 161ffvelrnd 6253 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔) ∈ ((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)))
16330, 31, 56, 55, 129, 132, 134, 136, 150, 162funcco 16300 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑧))‘((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘(((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔))(⟨(𝐹‘(𝐹𝑢)), (𝐹‘(𝐹𝑣))⟩(comp‘𝑌)(𝐹‘(𝐹𝑧)))(((𝐹𝑢)𝐺(𝐹𝑣))‘(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))))
164140, 141opeq12d 4342 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ⟨(𝐹‘(𝐹𝑢)), (𝐹‘(𝐹𝑣))⟩ = ⟨𝑢, 𝑣⟩)
165164, 153oveq12d 6545 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (⟨(𝐹‘(𝐹𝑢)), (𝐹‘(𝐹𝑣))⟩(comp‘𝑌)(𝐹‘(𝐹𝑧))) = (⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧))
166 f1ocnvfv2 6411 . . . . . . . . . . . 12 ((((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧)) → (((𝐹𝑣)𝐺(𝐹𝑧))‘(((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)) = 𝑔)
167157, 161, 166syl2anc 690 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑣)𝐺(𝐹𝑧))‘(((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)) = 𝑔)
168 f1ocnvfv2 6411 . . . . . . . . . . . 12 ((((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) ∧ 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣)) → (((𝐹𝑢)𝐺(𝐹𝑣))‘(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)) = 𝑓)
169145, 149, 168syl2anc 690 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑣))‘(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)) = 𝑓)
170165, 167, 169oveq123d 6548 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((𝐹𝑣)𝐺(𝐹𝑧))‘(((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔))(⟨(𝐹‘(𝐹𝑢)), (𝐹‘(𝐹𝑣))⟩(comp‘𝑌)(𝐹‘(𝐹𝑧)))(((𝐹𝑢)𝐺(𝐹𝑣))‘(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
171163, 170eqtrd 2643 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑧))‘((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
17230, 31, 32, 137, 132, 136ffthf1o 16348 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))))
173140, 153oveq12d 6545 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) = (𝑢(Hom ‘𝑌)𝑧))
174 f1oeq3 6027 . . . . . . . . . . . 12 (((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) = (𝑢(Hom ‘𝑌)𝑧) → (((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) ↔ ((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧)))
175173, 174syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) ↔ ((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧)))
176172, 175mpbid 220 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧))
177663ad2ant1 1074 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑋 ∈ Cat)
17830, 31, 56, 177, 132, 134, 136, 150, 162catcocl 16115 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧)))
179 f1ocnvfv 6412 . . . . . . . . . 10 ((((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧) ∧ ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))) → ((((𝐹𝑢)𝐺(𝐹𝑧))‘((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (((𝐹𝑢)𝐺(𝐹𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))))
180176, 178, 179syl2anc 690 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((𝐹𝑢)𝐺(𝐹𝑧))‘((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (((𝐹𝑢)𝐺(𝐹𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))))
181171, 180mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)))
182 simpl 471 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑧) → 𝑥 = 𝑢)
183182fveq2d 6092 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑧) → (𝐹𝑥) = (𝐹𝑢))
184 simpr 475 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑧) → 𝑦 = 𝑧)
185184fveq2d 6092 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑧) → (𝐹𝑦) = (𝐹𝑧))
186183, 185oveq12d 6545 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑧) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑧)))
187186cnveqd 5208 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑧) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑧)))
188 ovex 6555 . . . . . . . . . . . 12 ((𝐹𝑢)𝐺(𝐹𝑧)) ∈ V
189188cnvex 6983 . . . . . . . . . . 11 ((𝐹𝑢)𝐺(𝐹𝑧)) ∈ V
190187, 17, 189ovmpt2a 6667 . . . . . . . . . 10 ((𝑢𝑆𝑧𝑆) → (𝑢𝐻𝑧) = ((𝐹𝑢)𝐺(𝐹𝑧)))
191131, 135, 190syl2anc 690 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑧) = ((𝐹𝑢)𝐺(𝐹𝑧)))
192191fveq1d 6090 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (((𝐹𝑢)𝐺(𝐹𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)))
193 simpl 471 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑣𝑦 = 𝑧) → 𝑥 = 𝑣)
194193fveq2d 6092 . . . . . . . . . . . . . 14 ((𝑥 = 𝑣𝑦 = 𝑧) → (𝐹𝑥) = (𝐹𝑣))
195 simpr 475 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑣𝑦 = 𝑧) → 𝑦 = 𝑧)
196195fveq2d 6092 . . . . . . . . . . . . . 14 ((𝑥 = 𝑣𝑦 = 𝑧) → (𝐹𝑦) = (𝐹𝑧))
197194, 196oveq12d 6545 . . . . . . . . . . . . 13 ((𝑥 = 𝑣𝑦 = 𝑧) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑣)𝐺(𝐹𝑧)))
198197cnveqd 5208 . . . . . . . . . . . 12 ((𝑥 = 𝑣𝑦 = 𝑧) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑣)𝐺(𝐹𝑧)))
199 ovex 6555 . . . . . . . . . . . . 13 ((𝐹𝑣)𝐺(𝐹𝑧)) ∈ V
200199cnvex 6983 . . . . . . . . . . . 12 ((𝐹𝑣)𝐺(𝐹𝑧)) ∈ V
201198, 17, 200ovmpt2a 6667 . . . . . . . . . . 11 ((𝑣𝑆𝑧𝑆) → (𝑣𝐻𝑧) = ((𝐹𝑣)𝐺(𝐹𝑧)))
202133, 135, 201syl2anc 690 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑣𝐻𝑧) = ((𝐹𝑣)𝐺(𝐹𝑧)))
203202fveq1d 6090 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑣𝐻𝑧)‘𝑔) = (((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔))
204131, 133, 91syl2anc 690 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑣) = ((𝐹𝑢)𝐺(𝐹𝑣)))
205204fveq1d 6090 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑣)‘𝑓) = (((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))
206203, 205oveq12d 6545 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝑣𝐻𝑧)‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))((𝑢𝐻𝑣)‘𝑓)) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)))
207181, 192, 2063eqtr4d 2653 . . . . . . 7 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (((𝑣𝐻𝑧)‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))((𝑢𝐻𝑣)‘𝑓)))
20852, 30, 32, 31, 53, 54, 55, 56, 64, 66, 69, 73, 103, 128, 207isfuncd 16294 . . . . . 6 (𝜑𝐹(𝑌 Func 𝑋)𝐻)
20930, 51, 208cofuval2 16316 . . . . 5 (𝜑 → (⟨𝐹, 𝐻⟩ ∘func𝐹, 𝐺⟩) = ⟨(𝐹𝐹), (𝑢𝑅, 𝑣𝑅 ↦ (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣)))⟩)
210 eqid 2609 . . . . . 6 (idfunc𝑋) = (idfunc𝑋)
211210, 30, 66, 31idfuval 16305 . . . . 5 (𝜑 → (idfunc𝑋) = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
21246, 209, 2113eqtr4d 2653 . . . 4 (𝜑 → (⟨𝐹, 𝐻⟩ ∘func𝐹, 𝐺⟩) = (idfunc𝑋))
213 eqid 2609 . . . . 5 (comp‘𝐶) = (comp‘𝐶)
214 df-br 4578 . . . . . 6 (𝐹(𝑋 Func 𝑌)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
21551, 214sylib 206 . . . . 5 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
216 df-br 4578 . . . . . 6 (𝐹(𝑌 Func 𝑋)𝐻 ↔ ⟨𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
217208, 216sylib 206 . . . . 5 (𝜑 → ⟨𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
21857, 58, 59, 213, 65, 63, 65, 215, 217catcco 16520 . . . 4 (𝜑 → (⟨𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = (⟨𝐹, 𝐻⟩ ∘func𝐹, 𝐺⟩))
219 eqid 2609 . . . . 5 (Id‘𝐶) = (Id‘𝐶)
22057, 58, 219, 210, 59, 65catcid 16522 . . . 4 (𝜑 → ((Id‘𝐶)‘𝑋) = (idfunc𝑋))
221212, 218, 2203eqtr4d 2653 . . 3 (𝜑 → (⟨𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋))
222 eqid 2609 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
223 eqid 2609 . . . 4 (Sect‘𝐶) = (Sect‘𝐶)
22457catccat 16523 . . . . 5 (𝑈𝑉𝐶 ∈ Cat)
22559, 224syl 17 . . . 4 (𝜑𝐶 ∈ Cat)
22657, 58, 59, 222, 65, 63catchom 16518 . . . . 5 (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌))
227215, 226eleqtrrd 2690 . . . 4 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋(Hom ‘𝐶)𝑌))
22857, 58, 59, 222, 63, 65catchom 16518 . . . . 5 (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋))
229217, 228eleqtrrd 2690 . . . 4 (𝜑 → ⟨𝐹, 𝐻⟩ ∈ (𝑌(Hom ‘𝐶)𝑋))
23058, 222, 213, 219, 223, 225, 65, 63, 227, 229issect2 16183 . . 3 (𝜑 → (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨𝐹, 𝐻⟩ ↔ (⟨𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋)))
231221, 230mpbird 245 . 2 (𝜑 → ⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨𝐹, 𝐻⟩)
232 f1ococnv2 6061 . . . . . . 7 (𝐹:𝑅1-1-onto𝑆 → (𝐹𝐹) = ( I ↾ 𝑆))
2331, 232syl 17 . . . . . 6 (𝜑 → (𝐹𝐹) = ( I ↾ 𝑆))
234913adant1 1071 . . . . . . . . . 10 ((𝜑𝑢𝑆𝑣𝑆) → (𝑢𝐻𝑣) = ((𝐹𝑢)𝐺(𝐹𝑣)))
235234coeq2d 5194 . . . . . . . . 9 ((𝜑𝑢𝑆𝑣𝑆) → (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣)) = (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ ((𝐹𝑢)𝐺(𝐹𝑣))))
236333ad2ant1 1074 . . . . . . . . . . . 12 ((𝜑𝑢𝑆𝑣𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
237753adant3 1073 . . . . . . . . . . . 12 ((𝜑𝑢𝑆𝑣𝑆) → (𝐹𝑢) ∈ 𝑅)
238773adant2 1072 . . . . . . . . . . . 12 ((𝜑𝑢𝑆𝑣𝑆) → (𝐹𝑣) ∈ 𝑅)
23930, 31, 32, 236, 237, 238ffthf1o 16348 . . . . . . . . . . 11 ((𝜑𝑢𝑆𝑣𝑆) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))))
2401003impb 1251 . . . . . . . . . . . 12 ((𝜑𝑢𝑆𝑣𝑆) → ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
241240, 143syl 17 . . . . . . . . . . 11 ((𝜑𝑢𝑆𝑣𝑆) → (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) ↔ ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
242239, 241mpbid 220 . . . . . . . . . 10 ((𝜑𝑢𝑆𝑣𝑆) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
243 f1ococnv2 6061 . . . . . . . . . 10 (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ ((𝐹𝑢)𝐺(𝐹𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
244242, 243syl 17 . . . . . . . . 9 ((𝜑𝑢𝑆𝑣𝑆) → (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ ((𝐹𝑢)𝐺(𝐹𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
245235, 244eqtrd 2643 . . . . . . . 8 ((𝜑𝑢𝑆𝑣𝑆) → (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
246245mpt2eq3dva 6595 . . . . . . 7 (𝜑 → (𝑢𝑆, 𝑣𝑆 ↦ (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑢𝑆, 𝑣𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣))))
247 fveq2 6088 . . . . . . . . . 10 (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩))
248 df-ov 6530 . . . . . . . . . 10 (𝑢(Hom ‘𝑌)𝑣) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩)
249247, 248syl6eqr 2661 . . . . . . . . 9 (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = (𝑢(Hom ‘𝑌)𝑣))
250249reseq2d 5304 . . . . . . . 8 (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑌)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
251250mpt2mpt 6628 . . . . . . 7 (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))) = (𝑢𝑆, 𝑣𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
252246, 251syl6eqr 2661 . . . . . 6 (𝜑 → (𝑢𝑆, 𝑣𝑆 ↦ (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))))
253233, 252opeq12d 4342 . . . . 5 (𝜑 → ⟨(𝐹𝐹), (𝑢𝑆, 𝑣𝑆 ↦ (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣)))⟩ = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
25452, 208, 51cofuval2 16316 . . . . 5 (𝜑 → (⟨𝐹, 𝐺⟩ ∘func𝐹, 𝐻⟩) = ⟨(𝐹𝐹), (𝑢𝑆, 𝑣𝑆 ↦ (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣)))⟩)
255 eqid 2609 . . . . . 6 (idfunc𝑌) = (idfunc𝑌)
256255, 52, 64, 32idfuval 16305 . . . . 5 (𝜑 → (idfunc𝑌) = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
257253, 254, 2563eqtr4d 2653 . . . 4 (𝜑 → (⟨𝐹, 𝐺⟩ ∘func𝐹, 𝐻⟩) = (idfunc𝑌))
25857, 58, 59, 213, 63, 65, 63, 217, 215catcco 16520 . . . 4 (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨𝐹, 𝐻⟩) = (⟨𝐹, 𝐺⟩ ∘func𝐹, 𝐻⟩))
25957, 58, 219, 255, 59, 63catcid 16522 . . . 4 (𝜑 → ((Id‘𝐶)‘𝑌) = (idfunc𝑌))
260257, 258, 2593eqtr4d 2653 . . 3 (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌))
26158, 222, 213, 219, 223, 225, 63, 65, 229, 227issect2 16183 . . 3 (𝜑 → (⟨𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩ ↔ (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌)))
262260, 261mpbird 245 . 2 (𝜑 → ⟨𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)
263 catcisolem.i . . 3 𝐼 = (Inv‘𝐶)
26458, 263, 225, 65, 63, 223isinv 16189 . 2 (𝜑 → (⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨𝐹, 𝐻⟩ ↔ (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨𝐹, 𝐻⟩ ∧ ⟨𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)))
265231, 262, 264mpbir2and 958 1 (𝜑 → ⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨𝐹, 𝐻⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  cin 3538  cop 4130   class class class wbr 4577  cmpt 4637   I cid 4938   × cxp 5026  ccnv 5027  cres 5030  ccom 5032   Fn wfn 5785  wf 5786  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  cmpt2 6529  Basecbs 15641  Hom chom 15725  compcco 15726  Catccat 16094  Idccid 16095  Sectcsect 16173  Invcinv 16174   Func cfunc 16283  idfunccidfu 16284  func ccofu 16285   Full cful 16331   Faith cfth 16332  CatCatccatc 16513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-map 7723  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-fz 12153  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-hom 15739  df-cco 15740  df-cat 16098  df-cid 16099  df-sect 16176  df-inv 16177  df-func 16287  df-idfu 16288  df-cofu 16289  df-full 16333  df-fth 16334  df-catc 16514
This theorem is referenced by:  catciso  16526
  Copyright terms: Public domain W3C validator