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

Theorem catcisolem 16803
 Description: Lemma for catciso 16804. (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 6203 . . . . . . 7 (𝐹:𝑅1-1-onto𝑆 → (𝐹𝐹) = ( I ↾ 𝑅))
31, 2syl 17 . . . . . 6 (𝜑 → (𝐹𝐹) = ( I ↾ 𝑅))
413ad2ant1 1102 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑅𝑣𝑅) → 𝐹:𝑅1-1-onto𝑆)
5 f1of 6175 . . . . . . . . . . . . . 14 (𝐹:𝑅1-1-onto𝑆𝐹:𝑅𝑆)
64, 5syl 17 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → 𝐹:𝑅𝑆)
7 simp2 1082 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → 𝑢𝑅)
86, 7ffvelrnd 6400 . . . . . . . . . . . 12 ((𝜑𝑢𝑅𝑣𝑅) → (𝐹𝑢) ∈ 𝑆)
9 simp3 1083 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → 𝑣𝑅)
106, 9ffvelrnd 6400 . . . . . . . . . . . 12 ((𝜑𝑢𝑅𝑣𝑅) → (𝐹𝑣) ∈ 𝑆)
11 simpl 472 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → 𝑥 = (𝐹𝑢))
1211fveq2d 6233 . . . . . . . . . . . . . . 15 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → (𝐹𝑥) = (𝐹‘(𝐹𝑢)))
13 simpr 476 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → 𝑦 = (𝐹𝑣))
1413fveq2d 6233 . . . . . . . . . . . . . . 15 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → (𝐹𝑦) = (𝐹‘(𝐹𝑣)))
1512, 14oveq12d 6708 . . . . . . . . . . . . . 14 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))))
1615cnveqd 5330 . . . . . . . . . . . . 13 ((𝑥 = (𝐹𝑢) ∧ 𝑦 = (𝐹𝑣)) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))))
17 catcisolem.g . . . . . . . . . . . . 13 𝐻 = (𝑥𝑆, 𝑦𝑆((𝐹𝑥)𝐺(𝐹𝑦)))
18 ovex 6718 . . . . . . . . . . . . . 14 ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))) ∈ V
1918cnvex 7155 . . . . . . . . . . . . 13 ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))) ∈ V
2016, 17, 19ovmpt2a 6833 . . . . . . . . . . . 12 (((𝐹𝑢) ∈ 𝑆 ∧ (𝐹𝑣) ∈ 𝑆) → ((𝐹𝑢)𝐻(𝐹𝑣)) = ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))))
218, 10, 20syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑢𝑅𝑣𝑅) → ((𝐹𝑢)𝐻(𝐹𝑣)) = ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))))
22 f1ocnvfv1 6572 . . . . . . . . . . . . . 14 ((𝐹:𝑅1-1-onto𝑆𝑢𝑅) → (𝐹‘(𝐹𝑢)) = 𝑢)
234, 7, 22syl2anc 694 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → (𝐹‘(𝐹𝑢)) = 𝑢)
24 f1ocnvfv1 6572 . . . . . . . . . . . . . 14 ((𝐹:𝑅1-1-onto𝑆𝑣𝑅) → (𝐹‘(𝐹𝑣)) = 𝑣)
254, 9, 24syl2anc 694 . . . . . . . . . . . . 13 ((𝜑𝑢𝑅𝑣𝑅) → (𝐹‘(𝐹𝑣)) = 𝑣)
2623, 25oveq12d 6708 . . . . . . . . . . . 12 ((𝜑𝑢𝑅𝑣𝑅) → ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))) = (𝑢𝐺𝑣))
2726cnveqd 5330 . . . . . . . . . . 11 ((𝜑𝑢𝑅𝑣𝑅) → ((𝐹‘(𝐹𝑢))𝐺(𝐹‘(𝐹𝑣))) = (𝑢𝐺𝑣))
2821, 27eqtrd 2685 . . . . . . . . . 10 ((𝜑𝑢𝑅𝑣𝑅) → ((𝐹𝑢)𝐻(𝐹𝑣)) = (𝑢𝐺𝑣))
2928coeq1d 5316 . . . . . . . . 9 ((𝜑𝑢𝑅𝑣𝑅) → (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣)) = ((𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)))
30 catciso.r . . . . . . . . . . 11 𝑅 = (Base‘𝑋)
31 eqid 2651 . . . . . . . . . . 11 (Hom ‘𝑋) = (Hom ‘𝑋)
32 eqid 2651 . . . . . . . . . . 11 (Hom ‘𝑌) = (Hom ‘𝑌)
33 catcisolem.1 . . . . . . . . . . . 12 (𝜑𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
34333ad2ant1 1102 . . . . . . . . . . 11 ((𝜑𝑢𝑅𝑣𝑅) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
3530, 31, 32, 34, 7, 9ffthf1o 16626 . . . . . . . . . 10 ((𝜑𝑢𝑅𝑣𝑅) → (𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹𝑢)(Hom ‘𝑌)(𝐹𝑣)))
36 f1ococnv1 6203 . . . . . . . . . 10 ((𝑢𝐺𝑣):(𝑢(Hom ‘𝑋)𝑣)–1-1-onto→((𝐹𝑢)(Hom ‘𝑌)(𝐹𝑣)) → ((𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
3735, 36syl 17 . . . . . . . . 9 ((𝜑𝑢𝑅𝑣𝑅) → ((𝑢𝐺𝑣) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
3829, 37eqtrd 2685 . . . . . . . 8 ((𝜑𝑢𝑅𝑣𝑅) → (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
3938mpt2eq3dva 6761 . . . . . . 7 (𝜑 → (𝑢𝑅, 𝑣𝑅 ↦ (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑢𝑅, 𝑣𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣))))
40 fveq2 6229 . . . . . . . . . 10 (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩))
41 df-ov 6693 . . . . . . . . . 10 (𝑢(Hom ‘𝑋)𝑣) = ((Hom ‘𝑋)‘⟨𝑢, 𝑣⟩)
4240, 41syl6eqr 2703 . . . . . . . . 9 (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑋)‘𝑧) = (𝑢(Hom ‘𝑋)𝑣))
4342reseq2d 5428 . . . . . . . 8 (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑋)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
4443mpt2mpt 6794 . . . . . . 7 (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))) = (𝑢𝑅, 𝑣𝑅 ↦ ( I ↾ (𝑢(Hom ‘𝑋)𝑣)))
4539, 44syl6eqr 2703 . . . . . 6 (𝜑 → (𝑢𝑅, 𝑣𝑅 ↦ (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣))) = (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧))))
463, 45opeq12d 4441 . . . . 5 (𝜑 → ⟨(𝐹𝐹), (𝑢𝑅, 𝑣𝑅 ↦ (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣)))⟩ = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
47 inss1 3866 . . . . . . . . 9 ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Full 𝑌)
48 fullfunc 16613 . . . . . . . . 9 (𝑋 Full 𝑌) ⊆ (𝑋 Func 𝑌)
4947, 48sstri 3645 . . . . . . . 8 ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Func 𝑌)
5049ssbri 4730 . . . . . . 7 (𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺𝐹(𝑋 Func 𝑌)𝐺)
5133, 50syl 17 . . . . . 6 (𝜑𝐹(𝑋 Func 𝑌)𝐺)
52 catciso.s . . . . . . 7 𝑆 = (Base‘𝑌)
53 eqid 2651 . . . . . . 7 (Id‘𝑌) = (Id‘𝑌)
54 eqid 2651 . . . . . . 7 (Id‘𝑋) = (Id‘𝑋)
55 eqid 2651 . . . . . . 7 (comp‘𝑌) = (comp‘𝑌)
56 eqid 2651 . . . . . . 7 (comp‘𝑋) = (comp‘𝑋)
57 catciso.c . . . . . . . . . 10 𝐶 = (CatCat‘𝑈)
58 catciso.b . . . . . . . . . 10 𝐵 = (Base‘𝐶)
59 catciso.u . . . . . . . . . 10 (𝜑𝑈𝑉)
6057, 58, 59catcbas 16794 . . . . . . . . 9 (𝜑𝐵 = (𝑈 ∩ Cat))
61 inss2 3867 . . . . . . . . 9 (𝑈 ∩ Cat) ⊆ Cat
6260, 61syl6eqss 3688 . . . . . . . 8 (𝜑𝐵 ⊆ Cat)
63 catciso.y . . . . . . . 8 (𝜑𝑌𝐵)
6462, 63sseldd 3637 . . . . . . 7 (𝜑𝑌 ∈ Cat)
65 catciso.x . . . . . . . 8 (𝜑𝑋𝐵)
6662, 65sseldd 3637 . . . . . . 7 (𝜑𝑋 ∈ Cat)
67 f1ocnv 6187 . . . . . . . 8 (𝐹:𝑅1-1-onto𝑆𝐹:𝑆1-1-onto𝑅)
68 f1of 6175 . . . . . . . 8 (𝐹:𝑆1-1-onto𝑅𝐹:𝑆𝑅)
691, 67, 683syl 18 . . . . . . 7 (𝜑𝐹:𝑆𝑅)
70 ovex 6718 . . . . . . . . . 10 ((𝐹𝑥)𝐺(𝐹𝑦)) ∈ V
7170cnvex 7155 . . . . . . . . 9 ((𝐹𝑥)𝐺(𝐹𝑦)) ∈ V
7217, 71fnmpt2i 7284 . . . . . . . 8 𝐻 Fn (𝑆 × 𝑆)
7372a1i 11 . . . . . . 7 (𝜑𝐻 Fn (𝑆 × 𝑆))
7433adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
7569ffvelrnda 6399 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → (𝐹𝑢) ∈ 𝑅)
7675adantrr 753 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝐹𝑢) ∈ 𝑅)
7769ffvelrnda 6399 . . . . . . . . . . 11 ((𝜑𝑣𝑆) → (𝐹𝑣) ∈ 𝑅)
7877adantrl 752 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝐹𝑣) ∈ 𝑅)
7930, 31, 32, 74, 76, 78ffthf1o 16626 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))))
80 f1ocnv 6187 . . . . . . . . 9 (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))–1-1-onto→((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
81 f1of 6175 . . . . . . . . 9 (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))–1-1-onto→((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
8279, 80, 813syl 18 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
83 simpl 472 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
8483fveq2d 6233 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐹𝑥) = (𝐹𝑢))
85 simpr 476 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
8685fveq2d 6233 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐹𝑦) = (𝐹𝑣))
8784, 86oveq12d 6708 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑣)))
8887cnveqd 5330 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑣)))
89 ovex 6718 . . . . . . . . . . . 12 ((𝐹𝑢)𝐺(𝐹𝑣)) ∈ V
9089cnvex 7155 . . . . . . . . . . 11 ((𝐹𝑢)𝐺(𝐹𝑣)) ∈ V
9188, 17, 90ovmpt2a 6833 . . . . . . . . . 10 ((𝑢𝑆𝑣𝑆) → (𝑢𝐻𝑣) = ((𝐹𝑢)𝐺(𝐹𝑣)))
9291adantl 481 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝑢𝐻𝑣) = ((𝐹𝑢)𝐺(𝐹𝑣)))
931adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → 𝐹:𝑅1-1-onto𝑆)
94 simprl 809 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → 𝑢𝑆)
95 f1ocnvfv2 6573 . . . . . . . . . . . 12 ((𝐹:𝑅1-1-onto𝑆𝑢𝑆) → (𝐹‘(𝐹𝑢)) = 𝑢)
9693, 94, 95syl2anc 694 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝐹‘(𝐹𝑢)) = 𝑢)
97 simprr 811 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → 𝑣𝑆)
98 f1ocnvfv2 6573 . . . . . . . . . . . 12 ((𝐹:𝑅1-1-onto𝑆𝑣𝑆) → (𝐹‘(𝐹𝑣)) = 𝑣)
9993, 97, 98syl2anc 694 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝐹‘(𝐹𝑣)) = 𝑣)
10096, 99oveq12d 6708 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
101100eqcomd 2657 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝑢(Hom ‘𝑌)𝑣) = ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))))
10292, 101feq12d 6071 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → ((𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)) ↔ ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣)))⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))))
10382, 102mpbird 247 . . . . . . 7 ((𝜑 ∧ (𝑢𝑆𝑣𝑆)) → (𝑢𝐻𝑣):(𝑢(Hom ‘𝑌)𝑣)⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
104 simpr 476 . . . . . . . . . 10 ((𝜑𝑢𝑆) → 𝑢𝑆)
105 simpl 472 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑢) → 𝑥 = 𝑢)
106105fveq2d 6233 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑢) → (𝐹𝑥) = (𝐹𝑢))
107 simpr 476 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑢) → 𝑦 = 𝑢)
108107fveq2d 6233 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑢) → (𝐹𝑦) = (𝐹𝑢))
109106, 108oveq12d 6708 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑢) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑢)))
110109cnveqd 5330 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑢) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑢)))
111 ovex 6718 . . . . . . . . . . . 12 ((𝐹𝑢)𝐺(𝐹𝑢)) ∈ V
112111cnvex 7155 . . . . . . . . . . 11 ((𝐹𝑢)𝐺(𝐹𝑢)) ∈ V
113110, 17, 112ovmpt2a 6833 . . . . . . . . . 10 ((𝑢𝑆𝑢𝑆) → (𝑢𝐻𝑢) = ((𝐹𝑢)𝐺(𝐹𝑢)))
114104, 104, 113syl2anc 694 . . . . . . . . 9 ((𝜑𝑢𝑆) → (𝑢𝐻𝑢) = ((𝐹𝑢)𝐺(𝐹𝑢)))
115114fveq1d 6231 . . . . . . . 8 ((𝜑𝑢𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑌)‘𝑢)))
11651adantr 480 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → 𝐹(𝑋 Func 𝑌)𝐺)
11730, 54, 53, 116, 75funcid 16577 . . . . . . . . . 10 ((𝜑𝑢𝑆) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑋)‘(𝐹𝑢))) = ((Id‘𝑌)‘(𝐹‘(𝐹𝑢))))
1181, 95sylan 487 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → (𝐹‘(𝐹𝑢)) = 𝑢)
119118fveq2d 6233 . . . . . . . . . 10 ((𝜑𝑢𝑆) → ((Id‘𝑌)‘(𝐹‘(𝐹𝑢))) = ((Id‘𝑌)‘𝑢))
120117, 119eqtrd 2685 . . . . . . . . 9 ((𝜑𝑢𝑆) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑋)‘(𝐹𝑢))) = ((Id‘𝑌)‘𝑢))
12133adantr 480 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
12230, 31, 32, 121, 75, 75ffthf1o 16626 . . . . . . . . . 10 ((𝜑𝑢𝑆) → ((𝐹𝑢)𝐺(𝐹𝑢)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑢))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑢))))
12366adantr 480 . . . . . . . . . . 11 ((𝜑𝑢𝑆) → 𝑋 ∈ Cat)
12430, 31, 54, 123, 75catidcl 16390 . . . . . . . . . 10 ((𝜑𝑢𝑆) → ((Id‘𝑋)‘(𝐹𝑢)) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑢)))
125 f1ocnvfv 6574 . . . . . . . . . 10 ((((𝐹𝑢)𝐺(𝐹𝑢)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑢))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑢))) ∧ ((Id‘𝑋)‘(𝐹𝑢)) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑢))) → ((((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑋)‘(𝐹𝑢))) = ((Id‘𝑌)‘𝑢) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(𝐹𝑢))))
126122, 124, 125syl2anc 694 . . . . . . . . 9 ((𝜑𝑢𝑆) → ((((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑋)‘(𝐹𝑢))) = ((Id‘𝑌)‘𝑢) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(𝐹𝑢))))
127120, 126mpd 15 . . . . . . . 8 ((𝜑𝑢𝑆) → (((𝐹𝑢)𝐺(𝐹𝑢))‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(𝐹𝑢)))
128115, 127eqtrd 2685 . . . . . . 7 ((𝜑𝑢𝑆) → ((𝑢𝐻𝑢)‘((Id‘𝑌)‘𝑢)) = ((Id‘𝑋)‘(𝐹𝑢)))
129513ad2ant1 1102 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹(𝑋 Func 𝑌)𝐺)
130693ad2ant1 1102 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹:𝑆𝑅)
131 simp21 1114 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑢𝑆)
132130, 131ffvelrnd 6400 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹𝑢) ∈ 𝑅)
133 simp22 1115 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑣𝑆)
134130, 133ffvelrnd 6400 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹𝑣) ∈ 𝑅)
135 simp23 1116 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑧𝑆)
136130, 135ffvelrnd 6400 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹𝑧) ∈ 𝑅)
137333ad2ant1 1102 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
13830, 31, 32, 137, 132, 134ffthf1o 16626 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))))
13913ad2ant1 1102 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝐹:𝑅1-1-onto𝑆)
140139, 131, 95syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(𝐹𝑢)) = 𝑢)
141139, 133, 98syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(𝐹𝑣)) = 𝑣)
142140, 141oveq12d 6708 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
143 f1oeq3 6167 . . . . . . . . . . . . . . 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 222 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
146 f1ocnv 6187 . . . . . . . . . . . . 13 (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → ((𝐹𝑢)𝐺(𝐹𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
147 f1of 6175 . . . . . . . . . . . . 13 (((𝐹𝑢)𝐺(𝐹𝑣)):(𝑢(Hom ‘𝑌)𝑣)–1-1-onto→((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)) → ((𝐹𝑢)𝐺(𝐹𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
148145, 146, 1473syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑣)):(𝑢(Hom ‘𝑌)𝑣)⟶((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
149 simp3l 1109 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣))
150148, 149ffvelrnd 6400 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣)))
15130, 31, 32, 137, 134, 136ffthf1o 16626 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→((𝐹‘(𝐹𝑣))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))))
152 f1ocnvfv2 6573 . . . . . . . . . . . . . . . . 17 ((𝐹:𝑅1-1-onto𝑆𝑧𝑆) → (𝐹‘(𝐹𝑧)) = 𝑧)
153139, 135, 152syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝐹‘(𝐹𝑧)) = 𝑧)
154141, 153oveq12d 6708 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(𝐹𝑣))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) = (𝑣(Hom ‘𝑌)𝑧))
155 f1oeq3 6167 . . . . . . . . . . . . . . 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 222 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧))
158 f1ocnv 6187 . . . . . . . . . . . . 13 (((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) → ((𝐹𝑣)𝐺(𝐹𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)))
159 f1of 6175 . . . . . . . . . . . . 13 (((𝐹𝑣)𝐺(𝐹𝑧)):(𝑣(Hom ‘𝑌)𝑧)–1-1-onto→((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)) → ((𝐹𝑣)𝐺(𝐹𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)))
160157, 158, 1593syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑣)𝐺(𝐹𝑧)):(𝑣(Hom ‘𝑌)𝑧)⟶((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)))
161 simp3r 1110 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))
162160, 161ffvelrnd 6400 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔) ∈ ((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧)))
16330, 31, 56, 55, 129, 132, 134, 136, 150, 162funcco 16578 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑧))‘((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘(((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔))(⟨(𝐹‘(𝐹𝑢)), (𝐹‘(𝐹𝑣))⟩(comp‘𝑌)(𝐹‘(𝐹𝑧)))(((𝐹𝑢)𝐺(𝐹𝑣))‘(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))))
164140, 141opeq12d 4441 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ⟨(𝐹‘(𝐹𝑢)), (𝐹‘(𝐹𝑣))⟩ = ⟨𝑢, 𝑣⟩)
165164, 153oveq12d 6708 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (⟨(𝐹‘(𝐹𝑢)), (𝐹‘(𝐹𝑣))⟩(comp‘𝑌)(𝐹‘(𝐹𝑧))) = (⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧))
166 f1ocnvfv2 6573 . . . . . . . . . . . 12 ((((𝐹𝑣)𝐺(𝐹𝑧)):((𝐹𝑣)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑣(Hom ‘𝑌)𝑧) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧)) → (((𝐹𝑣)𝐺(𝐹𝑧))‘(((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)) = 𝑔)
167157, 161, 166syl2anc 694 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑣)𝐺(𝐹𝑧))‘(((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)) = 𝑔)
168 f1ocnvfv2 6573 . . . . . . . . . . . 12 ((((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) ∧ 𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣)) → (((𝐹𝑢)𝐺(𝐹𝑣))‘(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)) = 𝑓)
169145, 149, 168syl2anc 694 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑣))‘(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)) = 𝑓)
170165, 167, 169oveq123d 6711 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((𝐹𝑣)𝐺(𝐹𝑧))‘(((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔))(⟨(𝐹‘(𝐹𝑢)), (𝐹‘(𝐹𝑣))⟩(comp‘𝑌)(𝐹‘(𝐹𝑧)))(((𝐹𝑢)𝐺(𝐹𝑣))‘(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
171163, 170eqtrd 2685 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑧))‘((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓))
17230, 31, 32, 137, 132, 136ffthf1o 16626 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))))
173140, 153oveq12d 6708 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑧))) = (𝑢(Hom ‘𝑌)𝑧))
174 f1oeq3 6167 . . . . . . . . . . . 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 222 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧))
177663ad2ant1 1102 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → 𝑋 ∈ Cat)
17830, 31, 56, 177, 132, 134, 136, 150, 162catcocl 16393 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧)))
179 f1ocnvfv 6574 . . . . . . . . . 10 ((((𝐹𝑢)𝐺(𝐹𝑧)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))–1-1-onto→(𝑢(Hom ‘𝑌)𝑧) ∧ ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)) ∈ ((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑧))) → ((((𝐹𝑢)𝐺(𝐹𝑧))‘((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (((𝐹𝑢)𝐺(𝐹𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))))
180176, 178, 179syl2anc 694 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((((𝐹𝑢)𝐺(𝐹𝑧))‘((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))) = (𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓) → (((𝐹𝑢)𝐺(𝐹𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))))
181171, 180mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝐹𝑢)𝐺(𝐹𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)))
182 simpl 472 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑧) → 𝑥 = 𝑢)
183182fveq2d 6233 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑧) → (𝐹𝑥) = (𝐹𝑢))
184 simpr 476 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑧) → 𝑦 = 𝑧)
185184fveq2d 6233 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑧) → (𝐹𝑦) = (𝐹𝑧))
186183, 185oveq12d 6708 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑧) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑧)))
187186cnveqd 5330 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑧) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑢)𝐺(𝐹𝑧)))
188 ovex 6718 . . . . . . . . . . . 12 ((𝐹𝑢)𝐺(𝐹𝑧)) ∈ V
189188cnvex 7155 . . . . . . . . . . 11 ((𝐹𝑢)𝐺(𝐹𝑧)) ∈ V
190187, 17, 189ovmpt2a 6833 . . . . . . . . . 10 ((𝑢𝑆𝑧𝑆) → (𝑢𝐻𝑧) = ((𝐹𝑢)𝐺(𝐹𝑧)))
191131, 135, 190syl2anc 694 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑧) = ((𝐹𝑢)𝐺(𝐹𝑧)))
192191fveq1d 6231 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (((𝐹𝑢)𝐺(𝐹𝑧))‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)))
193 simpl 472 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑣𝑦 = 𝑧) → 𝑥 = 𝑣)
194193fveq2d 6233 . . . . . . . . . . . . . 14 ((𝑥 = 𝑣𝑦 = 𝑧) → (𝐹𝑥) = (𝐹𝑣))
195 simpr 476 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑣𝑦 = 𝑧) → 𝑦 = 𝑧)
196195fveq2d 6233 . . . . . . . . . . . . . 14 ((𝑥 = 𝑣𝑦 = 𝑧) → (𝐹𝑦) = (𝐹𝑧))
197194, 196oveq12d 6708 . . . . . . . . . . . . 13 ((𝑥 = 𝑣𝑦 = 𝑧) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑣)𝐺(𝐹𝑧)))
198197cnveqd 5330 . . . . . . . . . . . 12 ((𝑥 = 𝑣𝑦 = 𝑧) → ((𝐹𝑥)𝐺(𝐹𝑦)) = ((𝐹𝑣)𝐺(𝐹𝑧)))
199 ovex 6718 . . . . . . . . . . . . 13 ((𝐹𝑣)𝐺(𝐹𝑧)) ∈ V
200199cnvex 7155 . . . . . . . . . . . 12 ((𝐹𝑣)𝐺(𝐹𝑧)) ∈ V
201198, 17, 200ovmpt2a 6833 . . . . . . . . . . 11 ((𝑣𝑆𝑧𝑆) → (𝑣𝐻𝑧) = ((𝐹𝑣)𝐺(𝐹𝑧)))
202133, 135, 201syl2anc 694 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑣𝐻𝑧) = ((𝐹𝑣)𝐺(𝐹𝑧)))
203202fveq1d 6231 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑣𝐻𝑧)‘𝑔) = (((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔))
204131, 133, 91syl2anc 694 . . . . . . . . . 10 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (𝑢𝐻𝑣) = ((𝐹𝑢)𝐺(𝐹𝑣)))
205204fveq1d 6231 . . . . . . . . 9 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑣)‘𝑓) = (((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓))
206203, 205oveq12d 6708 . . . . . . . 8 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → (((𝑣𝐻𝑧)‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))((𝑢𝐻𝑣)‘𝑓)) = ((((𝐹𝑣)𝐺(𝐹𝑧))‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))(((𝐹𝑢)𝐺(𝐹𝑣))‘𝑓)))
207181, 192, 2063eqtr4d 2695 . . . . . . 7 ((𝜑 ∧ (𝑢𝑆𝑣𝑆𝑧𝑆) ∧ (𝑓 ∈ (𝑢(Hom ‘𝑌)𝑣) ∧ 𝑔 ∈ (𝑣(Hom ‘𝑌)𝑧))) → ((𝑢𝐻𝑧)‘(𝑔(⟨𝑢, 𝑣⟩(comp‘𝑌)𝑧)𝑓)) = (((𝑣𝐻𝑧)‘𝑔)(⟨(𝐹𝑢), (𝐹𝑣)⟩(comp‘𝑋)(𝐹𝑧))((𝑢𝐻𝑣)‘𝑓)))
20852, 30, 32, 31, 53, 54, 55, 56, 64, 66, 69, 73, 103, 128, 207isfuncd 16572 . . . . . 6 (𝜑𝐹(𝑌 Func 𝑋)𝐻)
20930, 51, 208cofuval2 16594 . . . . 5 (𝜑 → (⟨𝐹, 𝐻⟩ ∘func𝐹, 𝐺⟩) = ⟨(𝐹𝐹), (𝑢𝑅, 𝑣𝑅 ↦ (((𝐹𝑢)𝐻(𝐹𝑣)) ∘ (𝑢𝐺𝑣)))⟩)
210 eqid 2651 . . . . . 6 (idfunc𝑋) = (idfunc𝑋)
211210, 30, 66, 31idfuval 16583 . . . . 5 (𝜑 → (idfunc𝑋) = ⟨( I ↾ 𝑅), (𝑧 ∈ (𝑅 × 𝑅) ↦ ( I ↾ ((Hom ‘𝑋)‘𝑧)))⟩)
21246, 209, 2113eqtr4d 2695 . . . 4 (𝜑 → (⟨𝐹, 𝐻⟩ ∘func𝐹, 𝐺⟩) = (idfunc𝑋))
213 eqid 2651 . . . . 5 (comp‘𝐶) = (comp‘𝐶)
214 df-br 4686 . . . . . 6 (𝐹(𝑋 Func 𝑌)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
21551, 214sylib 208 . . . . 5 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋 Func 𝑌))
216 df-br 4686 . . . . . 6 (𝐹(𝑌 Func 𝑋)𝐻 ↔ ⟨𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
217208, 216sylib 208 . . . . 5 (𝜑 → ⟨𝐹, 𝐻⟩ ∈ (𝑌 Func 𝑋))
21857, 58, 59, 213, 65, 63, 65, 215, 217catcco 16798 . . . 4 (𝜑 → (⟨𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = (⟨𝐹, 𝐻⟩ ∘func𝐹, 𝐺⟩))
219 eqid 2651 . . . . 5 (Id‘𝐶) = (Id‘𝐶)
22057, 58, 219, 210, 59, 65catcid 16800 . . . 4 (𝜑 → ((Id‘𝐶)‘𝑋) = (idfunc𝑋))
221212, 218, 2203eqtr4d 2695 . . 3 (𝜑 → (⟨𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋))
222 eqid 2651 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
223 eqid 2651 . . . 4 (Sect‘𝐶) = (Sect‘𝐶)
22457catccat 16801 . . . . 5 (𝑈𝑉𝐶 ∈ Cat)
22559, 224syl 17 . . . 4 (𝜑𝐶 ∈ Cat)
22657, 58, 59, 222, 65, 63catchom 16796 . . . . 5 (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌))
227215, 226eleqtrrd 2733 . . . 4 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑋(Hom ‘𝐶)𝑌))
22857, 58, 59, 222, 63, 65catchom 16796 . . . . 5 (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋))
229217, 228eleqtrrd 2733 . . . 4 (𝜑 → ⟨𝐹, 𝐻⟩ ∈ (𝑌(Hom ‘𝐶)𝑋))
23058, 222, 213, 219, 223, 225, 65, 63, 227, 229issect2 16461 . . 3 (𝜑 → (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨𝐹, 𝐻⟩ ↔ (⟨𝐹, 𝐻⟩(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)⟨𝐹, 𝐺⟩) = ((Id‘𝐶)‘𝑋)))
231221, 230mpbird 247 . 2 (𝜑 → ⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨𝐹, 𝐻⟩)
232 f1ococnv2 6201 . . . . . . 7 (𝐹:𝑅1-1-onto𝑆 → (𝐹𝐹) = ( I ↾ 𝑆))
2331, 232syl 17 . . . . . 6 (𝜑 → (𝐹𝐹) = ( I ↾ 𝑆))
234913adant1 1099 . . . . . . . . . 10 ((𝜑𝑢𝑆𝑣𝑆) → (𝑢𝐻𝑣) = ((𝐹𝑢)𝐺(𝐹𝑣)))
235234coeq2d 5317 . . . . . . . . 9 ((𝜑𝑢𝑆𝑣𝑆) → (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣)) = (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ ((𝐹𝑢)𝐺(𝐹𝑣))))
236333ad2ant1 1102 . . . . . . . . . . . 12 ((𝜑𝑢𝑆𝑣𝑆) → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)
237753adant3 1101 . . . . . . . . . . . 12 ((𝜑𝑢𝑆𝑣𝑆) → (𝐹𝑢) ∈ 𝑅)
238773adant2 1100 . . . . . . . . . . . 12 ((𝜑𝑢𝑆𝑣𝑆) → (𝐹𝑣) ∈ 𝑅)
23930, 31, 32, 236, 237, 238ffthf1o 16626 . . . . . . . . . . 11 ((𝜑𝑢𝑆𝑣𝑆) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))))
2401003impb 1279 . . . . . . . . . . . 12 ((𝜑𝑢𝑆𝑣𝑆) → ((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) = (𝑢(Hom ‘𝑌)𝑣))
241240, 143syl 17 . . . . . . . . . . 11 ((𝜑𝑢𝑆𝑣𝑆) → (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→((𝐹‘(𝐹𝑢))(Hom ‘𝑌)(𝐹‘(𝐹𝑣))) ↔ ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣)))
242239, 241mpbid 222 . . . . . . . . . 10 ((𝜑𝑢𝑆𝑣𝑆) → ((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣))
243 f1ococnv2 6201 . . . . . . . . . 10 (((𝐹𝑢)𝐺(𝐹𝑣)):((𝐹𝑢)(Hom ‘𝑋)(𝐹𝑣))–1-1-onto→(𝑢(Hom ‘𝑌)𝑣) → (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ ((𝐹𝑢)𝐺(𝐹𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
244242, 243syl 17 . . . . . . . . 9 ((𝜑𝑢𝑆𝑣𝑆) → (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ ((𝐹𝑢)𝐺(𝐹𝑣))) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
245235, 244eqtrd 2685 . . . . . . . 8 ((𝜑𝑢𝑆𝑣𝑆) → (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
246245mpt2eq3dva 6761 . . . . . . 7 (𝜑 → (𝑢𝑆, 𝑣𝑆 ↦ (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑢𝑆, 𝑣𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣))))
247 fveq2 6229 . . . . . . . . . 10 (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩))
248 df-ov 6693 . . . . . . . . . 10 (𝑢(Hom ‘𝑌)𝑣) = ((Hom ‘𝑌)‘⟨𝑢, 𝑣⟩)
249247, 248syl6eqr 2703 . . . . . . . . 9 (𝑧 = ⟨𝑢, 𝑣⟩ → ((Hom ‘𝑌)‘𝑧) = (𝑢(Hom ‘𝑌)𝑣))
250249reseq2d 5428 . . . . . . . 8 (𝑧 = ⟨𝑢, 𝑣⟩ → ( I ↾ ((Hom ‘𝑌)‘𝑧)) = ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
251250mpt2mpt 6794 . . . . . . 7 (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))) = (𝑢𝑆, 𝑣𝑆 ↦ ( I ↾ (𝑢(Hom ‘𝑌)𝑣)))
252246, 251syl6eqr 2703 . . . . . 6 (𝜑 → (𝑢𝑆, 𝑣𝑆 ↦ (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧))))
253233, 252opeq12d 4441 . . . . 5 (𝜑 → ⟨(𝐹𝐹), (𝑢𝑆, 𝑣𝑆 ↦ (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣)))⟩ = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
25452, 208, 51cofuval2 16594 . . . . 5 (𝜑 → (⟨𝐹, 𝐺⟩ ∘func𝐹, 𝐻⟩) = ⟨(𝐹𝐹), (𝑢𝑆, 𝑣𝑆 ↦ (((𝐹𝑢)𝐺(𝐹𝑣)) ∘ (𝑢𝐻𝑣)))⟩)
255 eqid 2651 . . . . . 6 (idfunc𝑌) = (idfunc𝑌)
256255, 52, 64, 32idfuval 16583 . . . . 5 (𝜑 → (idfunc𝑌) = ⟨( I ↾ 𝑆), (𝑧 ∈ (𝑆 × 𝑆) ↦ ( I ↾ ((Hom ‘𝑌)‘𝑧)))⟩)
257253, 254, 2563eqtr4d 2695 . . . 4 (𝜑 → (⟨𝐹, 𝐺⟩ ∘func𝐹, 𝐻⟩) = (idfunc𝑌))
25857, 58, 59, 213, 63, 65, 63, 217, 215catcco 16798 . . . 4 (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨𝐹, 𝐻⟩) = (⟨𝐹, 𝐺⟩ ∘func𝐹, 𝐻⟩))
25957, 58, 219, 255, 59, 63catcid 16800 . . . 4 (𝜑 → ((Id‘𝐶)‘𝑌) = (idfunc𝑌))
260257, 258, 2593eqtr4d 2695 . . 3 (𝜑 → (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌))
26158, 222, 213, 219, 223, 225, 63, 65, 229, 227issect2 16461 . . 3 (𝜑 → (⟨𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩ ↔ (⟨𝐹, 𝐺⟩(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)⟨𝐹, 𝐻⟩) = ((Id‘𝐶)‘𝑌)))
262260, 261mpbird 247 . 2 (𝜑 → ⟨𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)
263 catcisolem.i . . 3 𝐼 = (Inv‘𝐶)
26458, 263, 225, 65, 63, 223isinv 16467 . 2 (𝜑 → (⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨𝐹, 𝐻⟩ ↔ (⟨𝐹, 𝐺⟩(𝑋(Sect‘𝐶)𝑌)⟨𝐹, 𝐻⟩ ∧ ⟨𝐹, 𝐻⟩(𝑌(Sect‘𝐶)𝑋)⟨𝐹, 𝐺⟩)))
265231, 262, 264mpbir2and 977 1 (𝜑 → ⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨𝐹, 𝐻⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ∩ cin 3606  ⟨cop 4216   class class class wbr 4685   ↦ cmpt 4762   I cid 5052   × cxp 5141  ◡ccnv 5142   ↾ cres 5145   ∘ ccom 5147   Fn wfn 5921  ⟶wf 5922  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  Basecbs 15904  Hom chom 15999  compcco 16000  Catccat 16372  Idccid 16373  Sectcsect 16451  Invcinv 16452   Func cfunc 16561  idfunccidfu 16562   ∘func ccofu 16563   Full cful 16609   Faith cfth 16610  CatCatccatc 16791 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-fz 12365  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-hom 16013  df-cco 16014  df-cat 16376  df-cid 16377  df-sect 16454  df-inv 16455  df-func 16565  df-idfu 16566  df-cofu 16567  df-full 16611  df-fth 16612  df-catc 16792 This theorem is referenced by:  catciso  16804
 Copyright terms: Public domain W3C validator