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

Theorem cofucl 16529
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 2620 . . . 4 (Base‘𝐶) = (Base‘𝐶)
2 cofucl.f . . . 4 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
3 cofucl.g . . . 4 (𝜑𝐺 ∈ (𝐷 Func 𝐸))
41, 2, 3cofuval 16523 . . 3 (𝜑 → (𝐺func 𝐹) = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
51, 2, 3cofu1st 16524 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)) = ((1st𝐺) ∘ (1st𝐹)))
64fveq2d 6182 . . . . 5 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩))
7 fvex 6188 . . . . . . 7 (1st𝐺) ∈ V
8 fvex 6188 . . . . . . 7 (1st𝐹) ∈ V
97, 8coex 7103 . . . . . 6 ((1st𝐺) ∘ (1st𝐹)) ∈ V
10 fvex 6188 . . . . . . 7 (Base‘𝐶) ∈ V
1110, 10mpt2ex 7232 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) ∈ V
129, 11op2nd 7162 . . . . 5 (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
136, 12syl6eq 2670 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))))
145, 13opeq12d 4401 . . 3 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
154, 14eqtr4d 2657 . 2 (𝜑 → (𝐺func 𝐹) = ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩)
16 eqid 2620 . . . . . . 7 (Base‘𝐷) = (Base‘𝐷)
17 eqid 2620 . . . . . . 7 (Base‘𝐸) = (Base‘𝐸)
18 relfunc 16503 . . . . . . . 8 Rel (𝐷 Func 𝐸)
19 1st2ndbr 7202 . . . . . . . 8 ((Rel (𝐷 Func 𝐸) ∧ 𝐺 ∈ (𝐷 Func 𝐸)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2018, 3, 19sylancr 694 . . . . . . 7 (𝜑 → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
2116, 17, 20funcf1 16507 . . . . . 6 (𝜑 → (1st𝐺):(Base‘𝐷)⟶(Base‘𝐸))
22 relfunc 16503 . . . . . . . 8 Rel (𝐶 Func 𝐷)
23 1st2ndbr 7202 . . . . . . . 8 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
2422, 2, 23sylancr 694 . . . . . . 7 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
251, 16, 24funcf1 16507 . . . . . 6 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
26 fco 6045 . . . . . 6 (((1st𝐺):(Base‘𝐷)⟶(Base‘𝐸) ∧ (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷)) → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
2721, 25, 26syl2anc 692 . . . . 5 (𝜑 → ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
285feq1d 6017 . . . . 5 (𝜑 → ((1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ↔ ((1st𝐺) ∘ (1st𝐹)):(Base‘𝐶)⟶(Base‘𝐸)))
2927, 28mpbird 247 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
30 eqid 2620 . . . . . . 7 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
31 ovex 6663 . . . . . . . 8 (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∈ V
32 ovex 6663 . . . . . . . 8 (𝑥(2nd𝐹)𝑦) ∈ V
3331, 32coex 7103 . . . . . . 7 ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) ∈ V
3430, 33fnmpt2i 7224 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))
3513fneq1d 5969 . . . . . 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 2620 . . . . . . . . . . 11 (Hom ‘𝐷) = (Hom ‘𝐷)
38 eqid 2620 . . . . . . . . . . 11 (Hom ‘𝐸) = (Hom ‘𝐸)
3920adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
4025adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
41 simprl 793 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
4240, 41ffvelrnd 6346 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
43 simprr 795 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
4440, 43ffvelrnd 6346 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
4516, 37, 38, 39, 42, 44funcf2 16509 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
46 eqid 2620 . . . . . . . . . . 11 (Hom ‘𝐶) = (Hom ‘𝐶)
4724adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
481, 46, 37, 47, 41, 43funcf2 16509 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
49 fco 6045 . . . . . . . . . 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 692 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
51 ovex 6663 . . . . . . . . . 10 (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ∈ V
52 ovex 6663 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) ∈ V
5351, 52elmap 7871 . . . . . . . . 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 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
563adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸))
571, 55, 56, 41, 43cofu2nd 16526 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
581, 55, 56, 41cofu1 16525 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
591, 55, 56, 43cofu1 16525 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
6058, 59oveq12d 6653 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) = (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
6160oveq1d 6650 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)) = ((((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
6254, 57, 613eltr4d 2714 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
6362ralrimivva 2968 . . . . . 6 (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
64 fveq2 6178 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩))
65 df-ov 6638 . . . . . . . . 9 (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((2nd ‘(𝐺func 𝐹))‘⟨𝑥, 𝑦⟩)
6664, 65syl6eqr 2672 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺func 𝐹))‘𝑧) = (𝑥(2nd ‘(𝐺func 𝐹))𝑦))
67 vex 3198 . . . . . . . . . . . 12 𝑥 ∈ V
68 vex 3198 . . . . . . . . . . . 12 𝑦 ∈ V
6967, 68op1std 7163 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
7069fveq2d 6182 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(1st𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑥))
7167, 68op2ndd 7164 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
7271fveq2d 6182 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺func 𝐹))‘(2nd𝑧)) = ((1st ‘(𝐺func 𝐹))‘𝑦))
7370, 72oveq12d 6653 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) = (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)))
74 fveq2 6178 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩))
75 df-ov 6638 . . . . . . . . . 10 (𝑥(Hom ‘𝐶)𝑦) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩)
7674, 75syl6eqr 2672 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = (𝑥(Hom ‘𝐶)𝑦))
7773, 76oveq12d 6653 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) = ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
7866, 77eleq12d 2693 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (((2nd ‘(𝐺func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ↔ (𝑥(2nd ‘(𝐺func 𝐹))𝑦) ∈ ((((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦))))
7978ralxp 5252 . . . . . 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 6188 . . . . . 6 (2nd ‘(𝐺func 𝐹)) ∈ V
8281elixp 7900 . . . . 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 697 . . . 4 (𝜑 → (2nd ‘(𝐺func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺func 𝐹))‘(1st𝑧))(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
84 eqid 2620 . . . . . . . . . 10 (Id‘𝐶) = (Id‘𝐶)
85 eqid 2620 . . . . . . . . . 10 (Id‘𝐷) = (Id‘𝐷)
8624adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
87 simpr 477 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
881, 84, 85, 86, 87funcid 16511 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
8988fveq2d 6182 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))))
90 eqid 2620 . . . . . . . . 9 (Id‘𝐸) = (Id‘𝐸)
9120adantr 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
9225ffvelrnda 6345 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
9316, 85, 90, 91, 92funcid 16511 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((Id‘𝐷)‘((1st𝐹)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
9489, 93eqtrd 2654 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
952adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
963adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐷 Func 𝐸))
97 funcrcl 16504 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
982, 97syl 17 . . . . . . . . . . 11 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
9998simpld 475 . . . . . . . . . 10 (𝜑𝐶 ∈ Cat)
10099adantr 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
1011, 46, 84, 100, 87catidcl 16324 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
1021, 95, 96, 87, 87, 46, 101cofu2 16527 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑥))‘((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥))))
1031, 95, 96, 87cofu1 16525 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
104103fveq2d 6182 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)) = ((Id‘𝐸)‘((1st𝐺)‘((1st𝐹)‘𝑥))))
10594, 102, 1043eqtr4d 2664 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺func 𝐹))‘𝑥)))
10686adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
107 simplr 791 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ (Base‘𝐶))
108 simprlr 802 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ (Base‘𝐶))
1091, 46, 37, 106, 107, 108funcf2 16509 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
110 eqid 2620 . . . . . . . . . . . . 13 (comp‘𝐶) = (comp‘𝐶)
111100adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐶 ∈ Cat)
112 simprll 801 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ (Base‘𝐶))
113 simprrl 803 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
114 simprrr 804 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
1151, 46, 110, 111, 107, 112, 108, 113, 114catcocl 16327 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
116 fvco3 6262 . . . . . . . . . . . 12 (((𝑥(2nd𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
117109, 115, 116syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
118 eqid 2620 . . . . . . . . . . . . 13 (comp‘𝐷) = (comp‘𝐷)
1191, 46, 110, 118, 106, 107, 112, 108, 113, 114funcco 16512 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
120119fveq2d 6182 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧))‘(((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓))))
121 eqid 2620 . . . . . . . . . . . 12 (comp‘𝐸) = (comp‘𝐸)
12291adantr 481 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐺)(𝐷 Func 𝐸)(2nd𝐺))
12392adantr 481 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
12425adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
125124adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
126125, 112ffvelrnd 6346 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
127125, 108ffvelrnd 6346 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st𝐹)‘𝑧) ∈ (Base‘𝐷))
1281, 46, 37, 106, 107, 112funcf2 16509 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
129128, 113ffvelrnd 6346 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd𝐹)𝑦)‘𝑓) ∈ (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
1301, 46, 37, 106, 112, 108funcf2 16509 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑦(2nd𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
131130, 114ffvelrnd 6346 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd𝐹)𝑧)‘𝑔) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
13216, 37, 118, 121, 122, 123, 126, 127, 129, 131funcco 16512 . . . . . . . . . . 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 2658 . . . . . . . . . 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 481 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐹 ∈ (𝐶 Func 𝐷))
13596adantr 481 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐺 ∈ (𝐷 Func 𝐸))
1361, 134, 135, 107, 108cofu2nd 16526 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑧) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧)))
137136fveq1d 6180 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑧)) ∘ (𝑥(2nd𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
138103adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
1391, 134, 135, 112cofu1 16525 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
140138, 139opeq12d 4401 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩ = ⟨((1st𝐺)‘((1st𝐹)‘𝑥)), ((1st𝐺)‘((1st𝐹)‘𝑦))⟩)
1411, 134, 135, 108cofu1 16525 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺func 𝐹))‘𝑧) = ((1st𝐺)‘((1st𝐹)‘𝑧)))
142140, 141oveq12d 6653 . . . . . . . . . . 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 16527 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔) = ((((1st𝐹)‘𝑦)(2nd𝐺)((1st𝐹)‘𝑧))‘((𝑦(2nd𝐹)𝑧)‘𝑔)))
1441, 134, 135, 107, 112, 46, 113cofu2 16527 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦))‘((𝑥(2nd𝐹)𝑦)‘𝑓)))
145142, 143, 144oveq123d 6656 . . . . . . . . . 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 2664 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
147146anassrs 679 . . . . . . . 8 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
148147ralrimivva 2968 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
149148ralrimivva 2968 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺func 𝐹))‘𝑥), ((1st ‘(𝐺func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺func 𝐹))𝑦)‘𝑓)))
150105, 149jca 554 . . . . 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 2963 . . . 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 16504 . . . . . . 7 (𝐺 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1533, 152syl 17 . . . . . 6 (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
154153simprd 479 . . . . 5 (𝜑𝐸 ∈ Cat)
1551, 17, 46, 38, 84, 90, 110, 121, 99, 154isfunc 16505 . . . 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 1243 . . 3 (𝜑 → (1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)))
157 df-br 4645 . . 3 ((1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)) ↔ ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
158156, 157sylib 208 . 2 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
15915, 158eqeltrd 2699 1 (𝜑 → (𝐺func 𝐹) ∈ (𝐶 Func 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481  wcel 1988  wral 2909  cop 4174   class class class wbr 4644   × cxp 5102  ccom 5108  Rel wrel 5109   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  cmpt2 6637  1st c1st 7151  2nd c2nd 7152  𝑚 cmap 7842  Xcixp 7893  Basecbs 15838  Hom chom 15933  compcco 15934  Catccat 16306  Idccid 16307   Func cfunc 16495  func ccofu 16497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-1st 7153  df-2nd 7154  df-map 7844  df-ixp 7894  df-cat 16310  df-cid 16311  df-func 16499  df-cofu 16501
This theorem is referenced by:  cofuass  16530  cofull  16575  cofth  16576  catccatid  16733  1st2ndprf  16827  uncfcl  16856  uncf1  16857  uncf2  16858  yonedalem1  16893  yonedalem21  16894  yonedalem22  16899  funcrngcsetcALT  41764
  Copyright terms: Public domain W3C validator