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

Theorem cofucl 16313
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 2605 . . . 4 (Base‘𝐶) = (Base‘𝐶)
2 cofucl.f . . . 4 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
3 cofucl.g . . . 4 (𝜑𝐺 ∈ (𝐷 Func 𝐸))
41, 2, 3cofuval 16307 . . 3 (𝜑 → (𝐺func 𝐹) = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
51, 2, 3cofu1st 16308 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)) = ((1st𝐺) ∘ (1st𝐹)))
64fveq2d 6088 . . . . 5 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩))
7 fvex 6094 . . . . . . 7 (1st𝐺) ∈ V
8 fvex 6094 . . . . . . 7 (1st𝐹) ∈ V
97, 8coex 6984 . . . . . 6 ((1st𝐺) ∘ (1st𝐹)) ∈ V
10 fvex 6094 . . . . . . 7 (Base‘𝐶) ∈ V
1110, 10mpt2ex 7109 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) ∈ V
129, 11op2nd 7041 . . . . 5 (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
136, 12syl6eq 2655 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))))
145, 13opeq12d 4338 . . 3 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
154, 14eqtr4d 2642 . 2 (𝜑 → (𝐺func 𝐹) = ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩)
16 eqid 2605 . . . . . . 7 (Base‘𝐷) = (Base‘𝐷)
17 eqid 2605 . . . . . . 7 (Base‘𝐸) = (Base‘𝐸)
18 relfunc 16287 . . . . . . . 8 Rel (𝐷 Func 𝐸)
19 1st2ndbr 7081 . . . . . . . 8 ((Rel (𝐷 Func 𝐸) ∧ 𝐺 ∈ (𝐷 Func 𝐸)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2018, 3, 19sylancr 693 . . . . . . 7 (𝜑 → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2116, 17, 20funcf1 16291 . . . . . 6 (𝜑 → (1st𝐺):(Base‘𝐷)⟶(Base‘𝐸))
22 relfunc 16287 . . . . . . . 8 Rel (𝐶 Func 𝐷)
23 1st2ndbr 7081 . . . . . . . 8 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
2422, 2, 23sylancr 693 . . . . . . 7 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
251, 16, 24funcf1 16291 . . . . . 6 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
26 fco 5953 . . . . . 6 (((1st𝐺):(Base‘𝐷)⟶(Base‘𝐸) ∧ (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷)) → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
2721, 25, 26syl2anc 690 . . . . 5 (𝜑 → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
285feq1d 5925 . . . . 5 (𝜑 → ((1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ↔ ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸)))
2927, 28mpbird 245 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
30 eqid 2605 . . . . . . 7 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
31 ovex 6551 . . . . . . . 8 (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∈ V
32 ovex 6551 . . . . . . . 8 (𝑥(2nd𝐹)𝑦) ∈ V
3331, 32coex 6984 . . . . . . 7 ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ V
3430, 33fnmpt2i 7101 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))
3513fneq1d 5877 . . . . . 6 (𝜑 → ((2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))))
3634, 35mpbiri 246 . . . . 5 (𝜑 → (2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)))
37 eqid 2605 . . . . . . . . . . 11 (Hom ‘𝐷) = (Hom ‘𝐷)
38 eqid 2605 . . . . . . . . . . 11 (Hom ‘𝐸) = (Hom ‘𝐸)
3920adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
4025adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
41 simprl 789 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
4240, 41ffvelrnd 6249 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
43 simprr 791 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
4440, 43ffvelrnd 6249 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
4516, 37, 38, 39, 42, 44funcf2 16293 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
46 eqid 2605 . . . . . . . . . . 11 (Hom ‘𝐶) = (Hom ‘𝐶)
4724adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
481, 46, 37, 47, 41, 43funcf2 16293 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
49 fco 5953 . . . . . . . . . 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 690 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
51 ovex 6551 . . . . . . . . . 10 (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ∈ V
52 ovex 6551 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) ∈ V
5351, 52elmap 7745 . . . . . . . . 9 (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)) ↔ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
5450, 53sylibr 222 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
552adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
563adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸))
571, 55, 56, 41, 43cofu2nd 16310 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
581, 55, 56, 41cofu1 16309 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
591, 55, 56, 43cofu1 16309 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
6058, 59oveq12d 6541 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) = (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
6160oveq1d 6538 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)) = ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
6254, 57, 613eltr4d 2698 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
6362ralrimivva 2949 . . . . . 6 (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
64 fveq2 6084 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩))
65 df-ov 6526 . . . . . . . . 9 (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩)
6664, 65syl6eqr 2657 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = (𝑥(2nd ‘(𝐺func 𝐹))𝑦))
67 vex 3171 . . . . . . . . . . . 12 𝑥 ∈ V
68 vex 3171 . . . . . . . . . . . 12 𝑦 ∈ V
6967, 68op1std 7042 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
7069fveq2d 6088 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(1st𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑥))
7167, 68op2ndd 7043 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
7271fveq2d 6088 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(2nd𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑦))
7370, 72oveq12d 6541 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) = (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)))
74 fveq2 6084 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩))
75 df-ov 6526 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩)
7674, 75syl6eqr 2657 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = (𝑥(Hom ‘𝐶)𝑦))
7773, 76oveq12d 6541 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) = ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
7866, 77eleq12d 2677 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ↔ (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦))))
7978ralxp 5169 . . . . . 6 (∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ↔ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
8063, 79sylibr 222 . . . . 5 (𝜑 → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
81 fvex 6094 . . . . . 6 (2nd ‘(𝐺func 𝐹)) ∈ V
8281elixp 7774 . . . . 5 ((2nd ‘(𝐺func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ↔ ((2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧))))
8336, 80, 82sylanbrc 694 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
84 eqid 2605 . . . . . . . . . 10 (Id‘𝐶) = (Id‘𝐶)
85 eqid 2605 . . . . . . . . . 10 (Id‘𝐷) = (Id‘𝐷)
8624adantr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
87 simpr 475 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
881, 84, 85, 86, 87funcid 16295 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
8988fveq2d 6088 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))))
90 eqid 2605 . . . . . . . . 9 (Id‘𝐸) = (Id‘𝐸)
9120adantr 479 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
9225ffvelrnda 6248 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
9316, 85, 90, 91, 92funcid 16295 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
9489, 93eqtrd 2639 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
952adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
963adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐷 Func 𝐸))
97 funcrcl 16288 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
982, 97syl 17 . . . . . . . . . . 11 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
9998simpld 473 . . . . . . . . . 10 (𝜑𝐶 ∈ Cat)
10099adantr 479 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
1011, 46, 84, 100, 87catidcl 16108 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
1021, 95, 96, 87, 87, 46, 101cofu2 16311 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))))
1031, 95, 96, 87cofu1 16309 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
104103fveq2d 6088 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
10594, 102, 1043eqtr4d 2649 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)))
10686adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
107 simplr 787 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ (Base‘𝐶))
108 simprlr 798 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ (Base‘𝐶))
1091, 46, 37, 106, 107, 108funcf2 16293 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
110 eqid 2605 . . . . . . . . . . . . 13 (comp‘𝐶) = (comp‘𝐶)
111100adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐶 ∈ Cat)
112 simprll 797 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ (Base‘𝐶))
113 simprrl 799 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
114 simprrr 800 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
1151, 46, 110, 111, 107, 112, 108, 113, 114catcocl 16111 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
116 fvco3 6166 . . . . . . . . . . . 12 (((𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
117109, 115, 116syl2anc 690 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
118 eqid 2605 . . . . . . . . . . . . 13 (comp‘𝐷) = (comp‘𝐷)
1191, 46, 110, 118, 106, 107, 112, 108, 113, 114funcco 16296 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
120119fveq2d 6088 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘(((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓))))
121 eqid 2605 . . . . . . . . . . . 12 (comp‘𝐸) = (comp‘𝐸)
12291adantr 479 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
12392adantr 479 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
12425adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
125124adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
126125, 112ffvelrnd 6249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
127125, 108ffvelrnd 6249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑧) ∈ (Base‘𝐷))
1281, 46, 37, 106, 107, 112funcf2 16293 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
129128, 113ffvelrnd 6249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑦)‘𝑓) ∈ (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
1301, 46, 37, 106, 112, 108funcf2 16293 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑦(2nd𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
131130, 114ffvelrnd 6249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd𝐹)𝑧)‘𝑔) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
13216, 37, 118, 121, 122, 123, 126, 127, 129, 131funcco 16296 . . . . . . . . . . 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 2643 . . . . . . . . . 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 479 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐹 ∈ (𝐶 Func 𝐷))
13596adantr 479 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐺 ∈ (𝐷 Func 𝐸))
1361, 134, 135, 107, 108cofu2nd 16310 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑧) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧)))
137136fveq1d 6086 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
138103adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
1391, 134, 135, 112cofu1 16309 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
140138, 139opeq12d 4338 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩ = ⟨((1st𝐺)‘((1st𝐹)‘𝑥)), ((1st𝐺)‘((1st𝐹)‘𝑦))⟩)
1411, 134, 135, 108cofu1 16309 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑧) = ((1st𝐺)‘((1st𝐹)‘𝑧)))
142140, 141oveq12d 6541 . . . . . . . . . . 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 16311 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔) = ((((1st𝐹)‘𝑦)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑦(2nd𝐹)𝑧)‘𝑔)))
1441, 134, 135, 107, 112, 46, 113cofu2 16311 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦))‘((𝑥(2nd𝐹)𝑦)‘𝑓)))
145142, 143, 144oveq123d 6544 . . . . . . . . . 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 2649 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
147146anassrs 677 . . . . . . . 8 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
148147ralrimivva 2949 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
149148ralrimivva 2949 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
150105, 149jca 552 . . . . 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 2944 . . . 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 16288 . . . . . . 7 (𝐺 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1533, 152syl 17 . . . . . 6 (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
154153simprd 477 . . . . 5 (𝜑𝐸 ∈ Cat)
1551, 17, 46, 38, 84, 90, 110, 121, 99, 154isfunc 16289 . . . 4 (𝜑 → ((1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)) ↔ ((1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ∧ (2nd ‘(𝐺func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((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 1237 . . 3 (𝜑 → (1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)))
157 df-br 4574 . . 3 ((1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)) ↔ ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
158156, 157sylib 206 . 2 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
15915, 158eqeltrd 2683 1 (𝜑 → (𝐺func 𝐹) ∈ (𝐶 Func 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1975  wral 2891  cop 4126   class class class wbr 4573   × cxp 5022  ccom 5028  Rel wrel 5029   Fn wfn 5781  wf 5782  cfv 5786  (class class class)co 6523  cmpt2 6525  1st c1st 7030  2nd c2nd 7031  𝑚 cmap 7717  Xcixp 7767  Basecbs 15637  Hom chom 15721  compcco 15722  Catccat 16090  Idccid 16091   Func cfunc 16279  func ccofu 16281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-1st 7032  df-2nd 7033  df-map 7719  df-ixp 7768  df-cat 16094  df-cid 16095  df-func 16283  df-cofu 16285
This theorem is referenced by:  cofuass  16314  cofull  16359  cofth  16360  catccatid  16517  1st2ndprf  16611  uncfcl  16640  uncf1  16641  uncf2  16642  yonedalem1  16677  yonedalem21  16678  yonedalem22  16683  funcrngcsetcALT  41789
  Copyright terms: Public domain W3C validator