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

Theorem cofucl 16900
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 2825 . . . 4 (Base‘𝐶) = (Base‘𝐶)
2 cofucl.f . . . 4 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
3 cofucl.g . . . 4 (𝜑𝐺 ∈ (𝐷 Func 𝐸))
41, 2, 3cofuval 16894 . . 3 (𝜑 → (𝐺func 𝐹) = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
51, 2, 3cofu1st 16895 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)) = ((1st𝐺) ∘ (1st𝐹)))
64fveq2d 6437 . . . . 5 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩))
7 fvex 6446 . . . . . . 7 (1st𝐺) ∈ V
8 fvex 6446 . . . . . . 7 (1st𝐹) ∈ V
97, 8coex 7380 . . . . . 6 ((1st𝐺) ∘ (1st𝐹)) ∈ V
10 fvex 6446 . . . . . . 7 (Base‘𝐶) ∈ V
1110, 10mpt2ex 7510 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) ∈ V
129, 11op2nd 7437 . . . . 5 (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
136, 12syl6eq 2877 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))))
145, 13opeq12d 4631 . . 3 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
154, 14eqtr4d 2864 . 2 (𝜑 → (𝐺func 𝐹) = ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩)
16 eqid 2825 . . . . . . 7 (Base‘𝐷) = (Base‘𝐷)
17 eqid 2825 . . . . . . 7 (Base‘𝐸) = (Base‘𝐸)
18 relfunc 16874 . . . . . . . 8 Rel (𝐷 Func 𝐸)
19 1st2ndbr 7479 . . . . . . . 8 ((Rel (𝐷 Func 𝐸) ∧ 𝐺 ∈ (𝐷 Func 𝐸)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2018, 3, 19sylancr 583 . . . . . . 7 (𝜑 → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2116, 17, 20funcf1 16878 . . . . . 6 (𝜑 → (1st𝐺):(Base‘𝐷)⟶(Base‘𝐸))
22 relfunc 16874 . . . . . . . 8 Rel (𝐶 Func 𝐷)
23 1st2ndbr 7479 . . . . . . . 8 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
2422, 2, 23sylancr 583 . . . . . . 7 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
251, 16, 24funcf1 16878 . . . . . 6 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
26 fco 6295 . . . . . 6 (((1st𝐺):(Base‘𝐷)⟶(Base‘𝐸) ∧ (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷)) → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
2721, 25, 26syl2anc 581 . . . . 5 (𝜑 → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
285feq1d 6263 . . . . 5 (𝜑 → ((1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ↔ ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸)))
2927, 28mpbird 249 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
30 eqid 2825 . . . . . . 7 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
31 ovex 6937 . . . . . . . 8 (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∈ V
32 ovex 6937 . . . . . . . 8 (𝑥(2nd𝐹)𝑦) ∈ V
3331, 32coex 7380 . . . . . . 7 ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ V
3430, 33fnmpt2i 7502 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))
3513fneq1d 6214 . . . . . 6 (𝜑 → ((2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))))
3634, 35mpbiri 250 . . . . 5 (𝜑 → (2nd ‘(𝐺func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)))
37 eqid 2825 . . . . . . . . . . 11 (Hom ‘𝐷) = (Hom ‘𝐷)
38 eqid 2825 . . . . . . . . . . 11 (Hom ‘𝐸) = (Hom ‘𝐸)
3920adantr 474 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
4025adantr 474 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
41 simprl 789 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
4240, 41ffvelrnd 6609 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
43 simprr 791 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
4440, 43ffvelrnd 6609 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
4516, 37, 38, 39, 42, 44funcf2 16880 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
46 eqid 2825 . . . . . . . . . . 11 (Hom ‘𝐶) = (Hom ‘𝐶)
4724adantr 474 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
481, 46, 37, 47, 41, 43funcf2 16880 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
49 fco 6295 . . . . . . . . . 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 581 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
51 ovex 6937 . . . . . . . . . 10 (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ∈ V
52 ovex 6937 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) ∈ V
5351, 52elmap 8151 . . . . . . . . 9 (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)) ↔ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
5450, 53sylibr 226 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
552adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
563adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸))
571, 55, 56, 41, 43cofu2nd 16897 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
581, 55, 56, 41cofu1 16896 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
591, 55, 56, 43cofu1 16896 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
6058, 59oveq12d 6923 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) = (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
6160oveq1d 6920 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)) = ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
6254, 57, 613eltr4d 2921 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
6362ralrimivva 3180 . . . . . 6 (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
64 fveq2 6433 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩))
65 df-ov 6908 . . . . . . . . 9 (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩)
6664, 65syl6eqr 2879 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = (𝑥(2nd ‘(𝐺func 𝐹))𝑦))
67 vex 3417 . . . . . . . . . . . 12 𝑥 ∈ V
68 vex 3417 . . . . . . . . . . . 12 𝑦 ∈ V
6967, 68op1std 7438 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
7069fveq2d 6437 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(1st𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑥))
7167, 68op2ndd 7439 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
7271fveq2d 6437 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(2nd𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑦))
7370, 72oveq12d 6923 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) = (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)))
74 fveq2 6433 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩))
75 df-ov 6908 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩)
7674, 75syl6eqr 2879 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = (𝑥(Hom ‘𝐶)𝑦))
7773, 76oveq12d 6923 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) = ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
7866, 77eleq12d 2900 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ↔ (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦))))
7978ralxp 5496 . . . . . 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 226 . . . . 5 (𝜑 → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
81 fvex 6446 . . . . . 6 (2nd ‘(𝐺func 𝐹)) ∈ V
8281elixp 8182 . . . . 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 580 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
84 eqid 2825 . . . . . . . . . 10 (Id‘𝐶) = (Id‘𝐶)
85 eqid 2825 . . . . . . . . . 10 (Id‘𝐷) = (Id‘𝐷)
8624adantr 474 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
87 simpr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
881, 84, 85, 86, 87funcid 16882 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
8988fveq2d 6437 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))))
90 eqid 2825 . . . . . . . . 9 (Id‘𝐸) = (Id‘𝐸)
9120adantr 474 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
9225ffvelrnda 6608 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
9316, 85, 90, 91, 92funcid 16882 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
9489, 93eqtrd 2861 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
952adantr 474 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
963adantr 474 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐷 Func 𝐸))
97 funcrcl 16875 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
982, 97syl 17 . . . . . . . . . . 11 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
9998simpld 490 . . . . . . . . . 10 (𝜑𝐶 ∈ Cat)
10099adantr 474 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
1011, 46, 84, 100, 87catidcl 16695 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
1021, 95, 96, 87, 87, 46, 101cofu2 16898 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))))
1031, 95, 96, 87cofu1 16896 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
104103fveq2d 6437 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
10594, 102, 1043eqtr4d 2871 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)))
10686adantr 474 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
107 simplr 787 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ (Base‘𝐶))
108 simprlr 800 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ (Base‘𝐶))
1091, 46, 37, 106, 107, 108funcf2 16880 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
110 eqid 2825 . . . . . . . . . . . . 13 (comp‘𝐶) = (comp‘𝐶)
111100adantr 474 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐶 ∈ Cat)
112 simprll 799 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ (Base‘𝐶))
113 simprrl 801 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
114 simprrr 802 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
1151, 46, 110, 111, 107, 112, 108, 113, 114catcocl 16698 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
116 fvco3 6522 . . . . . . . . . . . 12 (((𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
117109, 115, 116syl2anc 581 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
118 eqid 2825 . . . . . . . . . . . . 13 (comp‘𝐷) = (comp‘𝐷)
1191, 46, 110, 118, 106, 107, 112, 108, 113, 114funcco 16883 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
120119fveq2d 6437 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘(((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓))))
121 eqid 2825 . . . . . . . . . . . 12 (comp‘𝐸) = (comp‘𝐸)
12291adantr 474 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
12392adantr 474 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
12425adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
125124adantr 474 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
126125, 112ffvelrnd 6609 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
127125, 108ffvelrnd 6609 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑧) ∈ (Base‘𝐷))
1281, 46, 37, 106, 107, 112funcf2 16880 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
129128, 113ffvelrnd 6609 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑦)‘𝑓) ∈ (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
1301, 46, 37, 106, 112, 108funcf2 16880 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑦(2nd𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
131130, 114ffvelrnd 6609 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd𝐹)𝑧)‘𝑔) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
13216, 37, 118, 121, 122, 123, 126, 127, 129, 131funcco 16883 . . . . . . . . . . 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 2865 . . . . . . . . . 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 474 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐹 ∈ (𝐶 Func 𝐷))
13596adantr 474 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐺 ∈ (𝐷 Func 𝐸))
1361, 134, 135, 107, 108cofu2nd 16897 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑧) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧)))
137136fveq1d 6435 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
138103adantr 474 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
1391, 134, 135, 112cofu1 16896 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
140138, 139opeq12d 4631 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩ = ⟨((1st𝐺)‘((1st𝐹)‘𝑥)), ((1st𝐺)‘((1st𝐹)‘𝑦))⟩)
1411, 134, 135, 108cofu1 16896 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑧) = ((1st𝐺)‘((1st𝐹)‘𝑧)))
142140, 141oveq12d 6923 . . . . . . . . . . 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 16898 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔) = ((((1st𝐹)‘𝑦)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑦(2nd𝐹)𝑧)‘𝑔)))
1441, 134, 135, 107, 112, 46, 113cofu2 16898 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦))‘((𝑥(2nd𝐹)𝑦)‘𝑓)))
145142, 143, 144oveq123d 6926 . . . . . . . . . 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 2871 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
147146anassrs 461 . . . . . . . 8 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
148147ralrimivva 3180 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
149148ralrimivva 3180 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
150105, 149jca 509 . . . . 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 3175 . . . 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 16875 . . . . . . 7 (𝐺 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1533, 152syl 17 . . . . . 6 (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
154153simprd 491 . . . . 5 (𝜑𝐸 ∈ Cat)
1551, 17, 46, 38, 84, 90, 110, 121, 99, 154isfunc 16876 . . . 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 1448 . . 3 (𝜑 → (1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)))
157 df-br 4874 . . 3 ((1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)) ↔ ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
158156, 157sylib 210 . 2 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
15915, 158eqeltrd 2906 1 (𝜑 → (𝐺func 𝐹) ∈ (𝐶 Func 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1658  wcel 2166  wral 3117  cop 4403   class class class wbr 4873   × cxp 5340  ccom 5346  Rel wrel 5347   Fn wfn 6118  wf 6119  cfv 6123  (class class class)co 6905  cmpt2 6907  1st c1st 7426  2nd c2nd 7427  𝑚 cmap 8122  Xcixp 8175  Basecbs 16222  Hom chom 16316  compcco 16317  Catccat 16677  Idccid 16678   Func cfunc 16866  func ccofu 16868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-1st 7428  df-2nd 7429  df-map 8124  df-ixp 8176  df-cat 16681  df-cid 16682  df-func 16870  df-cofu 16872
This theorem is referenced by:  cofuass  16901  cofull  16946  cofth  16947  catccatid  17104  1st2ndprf  17199  uncfcl  17228  uncf1  17229  uncf2  17230  yonedalem1  17265  yonedalem21  17266  yonedalem22  17271  funcrngcsetcALT  42846
  Copyright terms: Public domain W3C validator