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

Theorem cofucl 16770
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 2761 . . . 4 (Base‘𝐶) = (Base‘𝐶)
2 cofucl.f . . . 4 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
3 cofucl.g . . . 4 (𝜑𝐺 ∈ (𝐷 Func 𝐸))
41, 2, 3cofuval 16764 . . 3 (𝜑 → (𝐺func 𝐹) = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
51, 2, 3cofu1st 16765 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)) = ((1st𝐺) ∘ (1st𝐹)))
64fveq2d 6358 . . . . 5 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩))
7 fvex 6364 . . . . . . 7 (1st𝐺) ∈ V
8 fvex 6364 . . . . . . 7 (1st𝐹) ∈ V
97, 8coex 7285 . . . . . 6 ((1st𝐺) ∘ (1st𝐹)) ∈ V
10 fvex 6364 . . . . . . 7 (Base‘𝐶) ∈ V
1110, 10mpt2ex 7417 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) ∈ V
129, 11op2nd 7344 . . . . 5 (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
136, 12syl6eq 2811 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))))
145, 13opeq12d 4562 . . 3 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
154, 14eqtr4d 2798 . 2 (𝜑 → (𝐺func 𝐹) = ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩)
16 eqid 2761 . . . . . . 7 (Base‘𝐷) = (Base‘𝐷)
17 eqid 2761 . . . . . . 7 (Base‘𝐸) = (Base‘𝐸)
18 relfunc 16744 . . . . . . . 8 Rel (𝐷 Func 𝐸)
19 1st2ndbr 7386 . . . . . . . 8 ((Rel (𝐷 Func 𝐸) ∧ 𝐺 ∈ (𝐷 Func 𝐸)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2018, 3, 19sylancr 698 . . . . . . 7 (𝜑 → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2116, 17, 20funcf1 16748 . . . . . 6 (𝜑 → (1st𝐺):(Base‘𝐷)⟶(Base‘𝐸))
22 relfunc 16744 . . . . . . . 8 Rel (𝐶 Func 𝐷)
23 1st2ndbr 7386 . . . . . . . 8 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
2422, 2, 23sylancr 698 . . . . . . 7 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
251, 16, 24funcf1 16748 . . . . . 6 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
26 fco 6220 . . . . . 6 (((1st𝐺):(Base‘𝐷)⟶(Base‘𝐸) ∧ (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷)) → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
2721, 25, 26syl2anc 696 . . . . 5 (𝜑 → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
285feq1d 6192 . . . . 5 (𝜑 → ((1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ↔ ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸)))
2927, 28mpbird 247 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
30 eqid 2761 . . . . . . 7 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
31 ovex 6843 . . . . . . . 8 (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∈ V
32 ovex 6843 . . . . . . . 8 (𝑥(2nd𝐹)𝑦) ∈ V
3331, 32coex 7285 . . . . . . 7 ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ V
3430, 33fnmpt2i 7409 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))
3513fneq1d 6143 . . . . . 6 (𝜑 → ((2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))))
3634, 35mpbiri 248 . . . . 5 (𝜑 → (2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)))
37 eqid 2761 . . . . . . . . . . 11 (Hom ‘𝐷) = (Hom ‘𝐷)
38 eqid 2761 . . . . . . . . . . 11 (Hom ‘𝐸) = (Hom ‘𝐸)
3920adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
4025adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
41 simprl 811 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
4240, 41ffvelrnd 6525 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
43 simprr 813 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
4440, 43ffvelrnd 6525 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
4516, 37, 38, 39, 42, 44funcf2 16750 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
46 eqid 2761 . . . . . . . . . . 11 (Hom ‘𝐶) = (Hom ‘𝐶)
4724adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
481, 46, 37, 47, 41, 43funcf2 16750 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
49 fco 6220 . . . . . . . . . 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 696 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
51 ovex 6843 . . . . . . . . . 10 (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ∈ V
52 ovex 6843 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) ∈ V
5351, 52elmap 8055 . . . . . . . . 9 (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)) ↔ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
5450, 53sylibr 224 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
552adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
563adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸))
571, 55, 56, 41, 43cofu2nd 16767 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
581, 55, 56, 41cofu1 16766 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
591, 55, 56, 43cofu1 16766 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
6058, 59oveq12d 6833 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) = (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
6160oveq1d 6830 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)) = ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
6254, 57, 613eltr4d 2855 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
6362ralrimivva 3110 . . . . . 6 (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
64 fveq2 6354 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩))
65 df-ov 6818 . . . . . . . . 9 (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩)
6664, 65syl6eqr 2813 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = (𝑥(2nd ‘(𝐺func 𝐹))𝑦))
67 vex 3344 . . . . . . . . . . . 12 𝑥 ∈ V
68 vex 3344 . . . . . . . . . . . 12 𝑦 ∈ V
6967, 68op1std 7345 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
7069fveq2d 6358 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(1st𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑥))
7167, 68op2ndd 7346 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
7271fveq2d 6358 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(2nd𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑦))
7370, 72oveq12d 6833 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) = (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)))
74 fveq2 6354 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩))
75 df-ov 6818 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩)
7674, 75syl6eqr 2813 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = (𝑥(Hom ‘𝐶)𝑦))
7773, 76oveq12d 6833 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) = ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
7866, 77eleq12d 2834 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ↔ (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦))))
7978ralxp 5420 . . . . . 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 224 . . . . 5 (𝜑 → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
81 fvex 6364 . . . . . 6 (2nd ‘(𝐺func 𝐹)) ∈ V
8281elixp 8084 . . . . 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 701 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
84 eqid 2761 . . . . . . . . . 10 (Id‘𝐶) = (Id‘𝐶)
85 eqid 2761 . . . . . . . . . 10 (Id‘𝐷) = (Id‘𝐷)
8624adantr 472 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
87 simpr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
881, 84, 85, 86, 87funcid 16752 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
8988fveq2d 6358 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))))
90 eqid 2761 . . . . . . . . 9 (Id‘𝐸) = (Id‘𝐸)
9120adantr 472 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
9225ffvelrnda 6524 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
9316, 85, 90, 91, 92funcid 16752 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
9489, 93eqtrd 2795 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
952adantr 472 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
963adantr 472 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐷 Func 𝐸))
97 funcrcl 16745 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
982, 97syl 17 . . . . . . . . . . 11 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
9998simpld 477 . . . . . . . . . 10 (𝜑𝐶 ∈ Cat)
10099adantr 472 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
1011, 46, 84, 100, 87catidcl 16565 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
1021, 95, 96, 87, 87, 46, 101cofu2 16768 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))))
1031, 95, 96, 87cofu1 16766 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
104103fveq2d 6358 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
10594, 102, 1043eqtr4d 2805 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)))
10686adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
107 simplr 809 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ (Base‘𝐶))
108 simprlr 822 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ (Base‘𝐶))
1091, 46, 37, 106, 107, 108funcf2 16750 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
110 eqid 2761 . . . . . . . . . . . . 13 (comp‘𝐶) = (comp‘𝐶)
111100adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐶 ∈ Cat)
112 simprll 821 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ (Base‘𝐶))
113 simprrl 823 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
114 simprrr 824 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
1151, 46, 110, 111, 107, 112, 108, 113, 114catcocl 16568 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
116 fvco3 6439 . . . . . . . . . . . 12 (((𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
117109, 115, 116syl2anc 696 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
118 eqid 2761 . . . . . . . . . . . . 13 (comp‘𝐷) = (comp‘𝐷)
1191, 46, 110, 118, 106, 107, 112, 108, 113, 114funcco 16753 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
120119fveq2d 6358 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘(((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓))))
121 eqid 2761 . . . . . . . . . . . 12 (comp‘𝐸) = (comp‘𝐸)
12291adantr 472 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
12392adantr 472 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
12425adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
125124adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
126125, 112ffvelrnd 6525 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
127125, 108ffvelrnd 6525 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑧) ∈ (Base‘𝐷))
1281, 46, 37, 106, 107, 112funcf2 16750 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
129128, 113ffvelrnd 6525 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑦)‘𝑓) ∈ (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
1301, 46, 37, 106, 112, 108funcf2 16750 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑦(2nd𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
131130, 114ffvelrnd 6525 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd𝐹)𝑧)‘𝑔) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
13216, 37, 118, 121, 122, 123, 126, 127, 129, 131funcco 16753 . . . . . . . . . . 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 2799 . . . . . . . . . 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 472 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐹 ∈ (𝐶 Func 𝐷))
13596adantr 472 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐺 ∈ (𝐷 Func 𝐸))
1361, 134, 135, 107, 108cofu2nd 16767 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑧) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧)))
137136fveq1d 6356 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
138103adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
1391, 134, 135, 112cofu1 16766 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
140138, 139opeq12d 4562 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩ = ⟨((1st𝐺)‘((1st𝐹)‘𝑥)), ((1st𝐺)‘((1st𝐹)‘𝑦))⟩)
1411, 134, 135, 108cofu1 16766 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑧) = ((1st𝐺)‘((1st𝐹)‘𝑧)))
142140, 141oveq12d 6833 . . . . . . . . . . 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 16768 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔) = ((((1st𝐹)‘𝑦)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑦(2nd𝐹)𝑧)‘𝑔)))
1441, 134, 135, 107, 112, 46, 113cofu2 16768 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦))‘((𝑥(2nd𝐹)𝑦)‘𝑓)))
145142, 143, 144oveq123d 6836 . . . . . . . . . 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 2805 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
147146anassrs 683 . . . . . . . 8 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
148147ralrimivva 3110 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
149148ralrimivva 3110 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
150105, 149jca 555 . . . . 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 3105 . . . 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 16745 . . . . . . 7 (𝐺 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1533, 152syl 17 . . . . . 6 (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
154153simprd 482 . . . . 5 (𝜑𝐸 ∈ Cat)
1551, 17, 46, 38, 84, 90, 110, 121, 99, 154isfunc 16746 . . . 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 1428 . . 3 (𝜑 → (1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)))
157 df-br 4806 . . 3 ((1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)) ↔ ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
158156, 157sylib 208 . 2 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
15915, 158eqeltrd 2840 1 (𝜑 → (𝐺func 𝐹) ∈ (𝐶 Func 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2140  wral 3051  cop 4328   class class class wbr 4805   × cxp 5265  ccom 5271  Rel wrel 5272   Fn wfn 6045  wf 6046  cfv 6050  (class class class)co 6815  cmpt2 6817  1st c1st 7333  2nd c2nd 7334  𝑚 cmap 8026  Xcixp 8077  Basecbs 16080  Hom chom 16175  compcco 16176  Catccat 16547  Idccid 16548   Func cfunc 16736  func ccofu 16738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-1st 7335  df-2nd 7336  df-map 8028  df-ixp 8078  df-cat 16551  df-cid 16552  df-func 16740  df-cofu 16742
This theorem is referenced by:  cofuass  16771  cofull  16816  cofth  16817  catccatid  16974  1st2ndprf  17068  uncfcl  17097  uncf1  17098  uncf2  17099  yonedalem1  17134  yonedalem21  17135  yonedalem22  17140  funcrngcsetcALT  42528
  Copyright terms: Public domain W3C validator