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

Theorem cofucl 17263
Description: The composition of two functors is a functor. Proposition 3.23 of [Adamek] p. 33. (Contributed by Mario Carneiro, 3-Jan-2017.)
Hypotheses
Ref Expression
cofucl.f (𝜑𝐹 ∈ (𝐶 Func 𝐷))
cofucl.g (𝜑𝐺 ∈ (𝐷 Func 𝐸))
Assertion
Ref Expression
cofucl (𝜑 → (𝐺func 𝐹) ∈ (𝐶 Func 𝐸))

Proof of Theorem cofucl
Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2738 . . . 4 (Base‘𝐶) = (Base‘𝐶)
2 cofucl.f . . . 4 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
3 cofucl.g . . . 4 (𝜑𝐺 ∈ (𝐷 Func 𝐸))
41, 2, 3cofuval 17257 . . 3 (𝜑 → (𝐺func 𝐹) = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
51, 2, 3cofu1st 17258 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)) = ((1st𝐺) ∘ (1st𝐹)))
64fveq2d 6678 . . . . 5 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩))
7 fvex 6687 . . . . . . 7 (1st𝐺) ∈ V
8 fvex 6687 . . . . . . 7 (1st𝐹) ∈ V
97, 8coex 7661 . . . . . 6 ((1st𝐺) ∘ (1st𝐹)) ∈ V
10 fvex 6687 . . . . . . 7 (Base‘𝐶) ∈ V
1110, 10mpoex 7803 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) ∈ V
129, 11op2nd 7723 . . . . 5 (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
136, 12eqtrdi 2789 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))))
145, 13opeq12d 4769 . . 3 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
154, 14eqtr4d 2776 . 2 (𝜑 → (𝐺func 𝐹) = ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩)
16 eqid 2738 . . . . . . 7 (Base‘𝐷) = (Base‘𝐷)
17 eqid 2738 . . . . . . 7 (Base‘𝐸) = (Base‘𝐸)
18 relfunc 17237 . . . . . . . 8 Rel (𝐷 Func 𝐸)
19 1st2ndbr 7766 . . . . . . . 8 ((Rel (𝐷 Func 𝐸) ∧ 𝐺 ∈ (𝐷 Func 𝐸)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2018, 3, 19sylancr 590 . . . . . . 7 (𝜑 → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2116, 17, 20funcf1 17241 . . . . . 6 (𝜑 → (1st𝐺):(Base‘𝐷)⟶(Base‘𝐸))
22 relfunc 17237 . . . . . . . 8 Rel (𝐶 Func 𝐷)
23 1st2ndbr 7766 . . . . . . . 8 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
2422, 2, 23sylancr 590 . . . . . . 7 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
251, 16, 24funcf1 17241 . . . . . 6 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
26 fco 6528 . . . . . 6 (((1st𝐺):(Base‘𝐷)⟶(Base‘𝐸) ∧ (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷)) → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
2721, 25, 26syl2anc 587 . . . . 5 (𝜑 → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
285feq1d 6489 . . . . 5 (𝜑 → ((1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ↔ ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸)))
2927, 28mpbird 260 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
30 eqid 2738 . . . . . . 7 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
31 ovex 7203 . . . . . . . 8 (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∈ V
32 ovex 7203 . . . . . . . 8 (𝑥(2nd𝐹)𝑦) ∈ V
3331, 32coex 7661 . . . . . . 7 ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ V
3430, 33fnmpoi 7793 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))
3513fneq1d 6431 . . . . . 6 (𝜑 → ((2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))))
3634, 35mpbiri 261 . . . . 5 (𝜑 → (2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)))
37 eqid 2738 . . . . . . . . . . 11 (Hom ‘𝐷) = (Hom ‘𝐷)
38 eqid 2738 . . . . . . . . . . 11 (Hom ‘𝐸) = (Hom ‘𝐸)
3920adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
4025adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
41 simprl 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
4240, 41ffvelrnd 6862 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
43 simprr 773 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
4440, 43ffvelrnd 6862 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
4516, 37, 38, 39, 42, 44funcf2 17243 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
46 eqid 2738 . . . . . . . . . . 11 (Hom ‘𝐶) = (Hom ‘𝐶)
4724adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
481, 46, 37, 47, 41, 43funcf2 17243 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
49 fco 6528 . . . . . . . . . 10 (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ∧ (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
5045, 48, 49syl2anc 587 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
51 ovex 7203 . . . . . . . . . 10 (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ∈ V
52 ovex 7203 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) ∈ V
5351, 52elmap 8481 . . . . . . . . 9 (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦)) ↔ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
5450, 53sylibr 237 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦)))
552adantr 484 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
563adantr 484 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸))
571, 55, 56, 41, 43cofu2nd 17260 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
581, 55, 56, 41cofu1 17259 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
591, 55, 56, 43cofu1 17259 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
6058, 59oveq12d 7188 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) = (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
6160oveq1d 7185 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)) = ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦)))
6254, 57, 613eltr4d 2848 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
6362ralrimivva 3103 . . . . . 6 (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
64 fveq2 6674 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩))
65 df-ov 7173 . . . . . . . . 9 (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩)
6664, 65eqtr4di 2791 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = (𝑥(2nd ‘(𝐺func 𝐹))𝑦))
67 vex 3402 . . . . . . . . . . . 12 𝑥 ∈ V
68 vex 3402 . . . . . . . . . . . 12 𝑦 ∈ V
6967, 68op1std 7724 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
7069fveq2d 6678 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(1st𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑥))
7167, 68op2ndd 7725 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
7271fveq2d 6678 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(2nd𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑦))
7370, 72oveq12d 7188 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) = (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)))
74 fveq2 6674 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩))
75 df-ov 7173 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩)
7674, 75eqtr4di 2791 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = (𝑥(Hom ‘𝐶)𝑦))
7773, 76oveq12d 7188 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) = ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
7866, 77eleq12d 2827 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦))))
7978ralxp 5684 . . . . . 6 (∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
8063, 79sylibr 237 . . . . 5 (𝜑 → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
81 fvex 6687 . . . . . 6 (2nd ‘(𝐺func 𝐹)) ∈ V
8281elixp 8514 . . . . 5 ((2nd ‘(𝐺func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ ((2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑m ((Hom ‘𝐶)‘𝑧))))
8336, 80, 82sylanbrc 586 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
84 eqid 2738 . . . . . . . . . 10 (Id‘𝐶) = (Id‘𝐶)
85 eqid 2738 . . . . . . . . . 10 (Id‘𝐷) = (Id‘𝐷)
8624adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
87 simpr 488 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
881, 84, 85, 86, 87funcid 17245 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
8988fveq2d 6678 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))))
90 eqid 2738 . . . . . . . . 9 (Id‘𝐸) = (Id‘𝐸)
9120adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
9225ffvelrnda 6861 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
9316, 85, 90, 91, 92funcid 17245 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
9489, 93eqtrd 2773 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
952adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
963adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐷 Func 𝐸))
97 funcrcl 17238 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
982, 97syl 17 . . . . . . . . . . 11 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
9998simpld 498 . . . . . . . . . 10 (𝜑𝐶 ∈ Cat)
10099adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
1011, 46, 84, 100, 87catidcl 17056 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
1021, 95, 96, 87, 87, 46, 101cofu2 17261 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))))
1031, 95, 96, 87cofu1 17259 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
104103fveq2d 6678 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
10594, 102, 1043eqtr4d 2783 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)))
10686adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
107 simplr 769 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ (Base‘𝐶))
108 simprlr 780 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ (Base‘𝐶))
1091, 46, 37, 106, 107, 108funcf2 17243 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
110 eqid 2738 . . . . . . . . . . . . 13 (comp‘𝐶) = (comp‘𝐶)
111100adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐶 ∈ Cat)
112 simprll 779 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ (Base‘𝐶))
113 simprrl 781 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
114 simprrr 782 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
1151, 46, 110, 111, 107, 112, 108, 113, 114catcocl 17059 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
116 fvco3 6767 . . . . . . . . . . . 12 (((𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
117109, 115, 116syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
118 eqid 2738 . . . . . . . . . . . . 13 (comp‘𝐷) = (comp‘𝐷)
1191, 46, 110, 118, 106, 107, 112, 108, 113, 114funcco 17246 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
120119fveq2d 6678 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘(((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓))))
121 eqid 2738 . . . . . . . . . . . 12 (comp‘𝐸) = (comp‘𝐸)
12291adantr 484 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
12392adantr 484 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
12425adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
125124adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
126125, 112ffvelrnd 6862 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
127125, 108ffvelrnd 6862 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑧) ∈ (Base‘𝐷))
1281, 46, 37, 106, 107, 112funcf2 17243 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
129128, 113ffvelrnd 6862 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑦)‘𝑓) ∈ (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
1301, 46, 37, 106, 112, 108funcf2 17243 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑦(2nd𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
131130, 114ffvelrnd 6862 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd𝐹)𝑧)‘𝑔) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
13216, 37, 118, 121, 122, 123, 126, 127, 129, 131funcco 17246 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘(((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓))) = (((((1st𝐹)‘𝑦)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑦(2nd𝐹)𝑧)‘𝑔))(⟨((1st𝐺)‘((1st𝐹)‘𝑥)), ((1st𝐺)‘((1st𝐹)‘𝑦))⟩(comp‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑧)))((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦))‘((𝑥(2nd𝐹)𝑦)‘𝑓))))
133117, 120, 1323eqtrd 2777 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st𝐹)‘𝑦)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑦(2nd𝐹)𝑧)‘𝑔))(⟨((1st𝐺)‘((1st𝐹)‘𝑥)), ((1st𝐺)‘((1st𝐹)‘𝑦))⟩(comp‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑧)))((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦))‘((𝑥(2nd𝐹)𝑦)‘𝑓))))
13495adantr 484 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐹 ∈ (𝐶 Func 𝐷))
13596adantr 484 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐺 ∈ (𝐷 Func 𝐸))
1361, 134, 135, 107, 108cofu2nd 17260 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑧) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧)))
137136fveq1d 6676 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
138103adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
1391, 134, 135, 112cofu1 17259 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
140138, 139opeq12d 4769 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩ = ⟨((1st𝐺)‘((1st𝐹)‘𝑥)), ((1st𝐺)‘((1st𝐹)‘𝑦))⟩)
1411, 134, 135, 108cofu1 17259 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑧) = ((1st𝐺)‘((1st𝐹)‘𝑧)))
142140, 141oveq12d 7188 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧)) = (⟨((1st𝐺)‘((1st𝐹)‘𝑥)), ((1st𝐺)‘((1st𝐹)‘𝑦))⟩(comp‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑧))))
1431, 134, 135, 112, 108, 46, 114cofu2 17261 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔) = ((((1st𝐹)‘𝑦)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑦(2nd𝐹)𝑧)‘𝑔)))
1441, 134, 135, 107, 112, 46, 113cofu2 17261 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦))‘((𝑥(2nd𝐹)𝑦)‘𝑓)))
145142, 143, 144oveq123d 7191 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)) = (((((1st𝐹)‘𝑦)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑦(2nd𝐹)𝑧)‘𝑔))(⟨((1st𝐺)‘((1st𝐹)‘𝑥)), ((1st𝐺)‘((1st𝐹)‘𝑦))⟩(comp‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑧)))((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦))‘((𝑥(2nd𝐹)𝑦)‘𝑓))))
146133, 137, 1453eqtr4d 2783 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
147146anassrs 471 . . . . . . . 8 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
148147ralrimivva 3103 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
149148ralrimivva 3103 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
150105, 149jca 515 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → (((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓))))
151150ralrimiva 3096 . . . 4 (𝜑 → ∀𝑥 ∈ (Base‘𝐶)(((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓))))
152 funcrcl 17238 . . . . . . 7 (𝐺 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1533, 152syl 17 . . . . . 6 (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
154153simprd 499 . . . . 5 (𝜑𝐸 ∈ Cat)
1551, 17, 46, 38, 84, 90, 110, 121, 99, 154isfunc 17239 . . . 4 (𝜑 → ((1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)) ↔ ((1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ∧ (2nd ‘(𝐺func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐶)(((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓))))))
15629, 83, 151, 155mpbir3and 1343 . . 3 (𝜑 → (1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)))
157 df-br 5031 . . 3 ((1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)) ↔ ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
158156, 157sylib 221 . 2 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
15915, 158eqeltrd 2833 1 (𝜑 → (𝐺func 𝐹) ∈ (𝐶 Func 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1542  wcel 2114  wral 3053  cop 4522   class class class wbr 5030   × cxp 5523  ccom 5529  Rel wrel 5530   Fn wfn 6334  wf 6335  cfv 6339  (class class class)co 7170  cmpo 7172  1st c1st 7712  2nd c2nd 7713  m cmap 8437  Xcixp 8507  Basecbs 16586  Hom chom 16679  compcco 16680  Catccat 17038  Idccid 17039   Func cfunc 17229  func ccofu 17231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-1st 7714  df-2nd 7715  df-map 8439  df-ixp 8508  df-cat 17042  df-cid 17043  df-func 17233  df-cofu 17235
This theorem is referenced by:  cofuass  17264  cofull  17309  cofth  17310  catccatid  17478  1st2ndprf  17572  uncfcl  17601  uncf1  17602  uncf2  17603  yonedalem1  17638  yonedalem21  17639  yonedalem22  17644  funcrngcsetcALT  45091
  Copyright terms: Public domain W3C validator