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

Theorem curfcl 17548
 Description: The curry functor of a functor 𝐹:𝐶 × 𝐷⟶𝐸 is a functor curryF (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Mario Carneiro, 13-Jan-2017.)
Hypotheses
Ref Expression
curfcl.g 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
curfcl.q 𝑄 = (𝐷 FuncCat 𝐸)
curfcl.c (𝜑𝐶 ∈ Cat)
curfcl.d (𝜑𝐷 ∈ Cat)
curfcl.f (𝜑𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
Assertion
Ref Expression
curfcl (𝜑𝐺 ∈ (𝐶 Func 𝑄))

Proof of Theorem curfcl
Dummy variables 𝑤 𝑔 𝑥 𝑦 𝑧 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 curfcl.g . . . 4 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
2 eqid 2758 . . . 4 (Base‘𝐶) = (Base‘𝐶)
3 curfcl.c . . . 4 (𝜑𝐶 ∈ Cat)
4 curfcl.d . . . 4 (𝜑𝐷 ∈ Cat)
5 curfcl.f . . . 4 (𝜑𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
6 eqid 2758 . . . 4 (Base‘𝐷) = (Base‘𝐷)
7 eqid 2758 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
8 eqid 2758 . . . 4 (Id‘𝐶) = (Id‘𝐶)
9 eqid 2758 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
10 eqid 2758 . . . 4 (Id‘𝐷) = (Id‘𝐷)
111, 2, 3, 4, 5, 6, 7, 8, 9, 10curfval 17539 . . 3 (𝜑𝐺 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))⟩)
12 fvex 6671 . . . . . . 7 (Base‘𝐶) ∈ V
1312mptex 6977 . . . . . 6 (𝑥 ∈ (Base‘𝐶) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩) ∈ V
1412, 12mpoex 7782 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))) ∈ V
1513, 14op1std 7703 . . . . 5 (𝐺 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))⟩ → (1st𝐺) = (𝑥 ∈ (Base‘𝐶) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩))
1611, 15syl 17 . . . 4 (𝜑 → (1st𝐺) = (𝑥 ∈ (Base‘𝐶) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩))
1713, 14op2ndd 7704 . . . . 5 (𝐺 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))⟩ → (2nd𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))))
1811, 17syl 17 . . . 4 (𝜑 → (2nd𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))))
1916, 18opeq12d 4771 . . 3 (𝜑 → ⟨(1st𝐺), (2nd𝐺)⟩ = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))⟩)
2011, 19eqtr4d 2796 . 2 (𝜑𝐺 = ⟨(1st𝐺), (2nd𝐺)⟩)
21 curfcl.q . . . . 5 𝑄 = (𝐷 FuncCat 𝐸)
2221fucbas 17289 . . . 4 (𝐷 Func 𝐸) = (Base‘𝑄)
23 eqid 2758 . . . . 5 (𝐷 Nat 𝐸) = (𝐷 Nat 𝐸)
2421, 23fuchom 17290 . . . 4 (𝐷 Nat 𝐸) = (Hom ‘𝑄)
25 eqid 2758 . . . 4 (Id‘𝑄) = (Id‘𝑄)
26 eqid 2758 . . . 4 (comp‘𝐶) = (comp‘𝐶)
27 eqid 2758 . . . 4 (comp‘𝑄) = (comp‘𝑄)
28 funcrcl 17192 . . . . . . 7 (𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸) → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
295, 28syl 17 . . . . . 6 (𝜑 → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
3029simprd 499 . . . . 5 (𝜑𝐸 ∈ Cat)
3121, 4, 30fuccat 17299 . . . 4 (𝜑𝑄 ∈ Cat)
32 opex 5324 . . . . . 6 ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩ ∈ V
3332a1i 11 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩ ∈ V)
343adantr 484 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
354adantr 484 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat)
365adantr 484 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
37 simpr 488 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
38 eqid 2758 . . . . . 6 ((1st𝐺)‘𝑥) = ((1st𝐺)‘𝑥)
391, 2, 34, 35, 36, 6, 37, 38curf1cl 17544 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐺)‘𝑥) ∈ (𝐷 Func 𝐸))
4033, 16, 39fmpt2d 6878 . . . 4 (𝜑 → (1st𝐺):(Base‘𝐶)⟶(𝐷 Func 𝐸))
41 eqid 2758 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))
42 ovex 7183 . . . . . . 7 (𝑥(Hom ‘𝐶)𝑦) ∈ V
4342mptex 6977 . . . . . 6 (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))) ∈ V
4441, 43fnmpoi 7772 . . . . 5 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))) Fn ((Base‘𝐶) × (Base‘𝐶))
4518fneq1d 6427 . . . . 5 (𝜑 → ((2nd𝐺) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))) Fn ((Base‘𝐶) × (Base‘𝐶))))
4644, 45mpbiri 261 . . . 4 (𝜑 → (2nd𝐺) Fn ((Base‘𝐶) × (Base‘𝐶)))
47 fvex 6671 . . . . . . 7 (Base‘𝐷) ∈ V
4847mptex 6977 . . . . . 6 (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) ∈ V
4948a1i 11 . . . . 5 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) ∈ V)
5018oveqd 7167 . . . . . 6 (𝜑 → (𝑥(2nd𝐺)𝑦) = (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))𝑦))
5141ovmpt4g 7292 . . . . . . 7 ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))) ∈ V) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))𝑦) = (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))
5243, 51mp3an3 1447 . . . . . 6 ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))𝑦) = (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))
5350, 52sylan9eq 2813 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐺)𝑦) = (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))
543ad2antrr 725 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐶 ∈ Cat)
554ad2antrr 725 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐷 ∈ Cat)
565ad2antrr 725 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
57 simplrl 776 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶))
58 simplrr 777 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶))
59 simpr 488 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦))
60 eqid 2758 . . . . . 6 ((𝑥(2nd𝐺)𝑦)‘𝑔) = ((𝑥(2nd𝐺)𝑦)‘𝑔)
611, 2, 54, 55, 56, 6, 9, 10, 57, 58, 59, 60, 23curf2cl 17547 . . . . 5 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd𝐺)𝑦)‘𝑔) ∈ (((1st𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st𝐺)‘𝑦)))
6249, 53, 61fmpt2d 6878 . . . 4 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st𝐺)‘𝑦)))
63 eqid 2758 . . . . . . . . . 10 (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
6463, 2, 6xpcbas 17494 . . . . . . . . 9 ((Base‘𝐶) × (Base‘𝐷)) = (Base‘(𝐶 ×c 𝐷))
65 eqid 2758 . . . . . . . . 9 (Id‘(𝐶 ×c 𝐷)) = (Id‘(𝐶 ×c 𝐷))
66 eqid 2758 . . . . . . . . 9 (Id‘𝐸) = (Id‘𝐸)
67 relfunc 17191 . . . . . . . . . . 11 Rel ((𝐶 ×c 𝐷) Func 𝐸)
68 1st2ndbr 7745 . . . . . . . . . . 11 ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
6967, 5, 68sylancr 590 . . . . . . . . . 10 (𝜑 → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
7069ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
71 opelxpi 5561 . . . . . . . . . 10 ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
7271adantll 713 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
7364, 65, 66, 70, 72funcid 17199 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑥, 𝑦⟩)) = ((Id‘𝐸)‘((1st𝐹)‘⟨𝑥, 𝑦⟩)))
743ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐶 ∈ Cat)
754ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat)
7637adantr 484 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝑥 ∈ (Base‘𝐶))
77 simpr 488 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝑦 ∈ (Base‘𝐷))
7863, 74, 75, 2, 6, 8, 10, 65, 76, 77xpcid 17505 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((Id‘(𝐶 ×c 𝐷))‘⟨𝑥, 𝑦⟩) = ⟨((Id‘𝐶)‘𝑥), ((Id‘𝐷)‘𝑦)⟩)
7978fveq2d 6662 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑥, 𝑦⟩)) = ((⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑥), ((Id‘𝐷)‘𝑦)⟩))
80 df-ov 7153 . . . . . . . . 9 (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑥), ((Id‘𝐷)‘𝑦)⟩)
8179, 80eqtr4di 2811 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑥, 𝑦⟩)) = (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)((Id‘𝐷)‘𝑦)))
825ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
831, 2, 74, 75, 82, 6, 76, 38, 77curf11 17542 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st ‘((1st𝐺)‘𝑥))‘𝑦) = (𝑥(1st𝐹)𝑦))
84 df-ov 7153 . . . . . . . . . 10 (𝑥(1st𝐹)𝑦) = ((1st𝐹)‘⟨𝑥, 𝑦⟩)
8583, 84eqtr2di 2810 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st𝐹)‘⟨𝑥, 𝑦⟩) = ((1st ‘((1st𝐺)‘𝑥))‘𝑦))
8685fveq2d 6662 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((Id‘𝐸)‘((1st𝐹)‘⟨𝑥, 𝑦⟩)) = ((Id‘𝐸)‘((1st ‘((1st𝐺)‘𝑥))‘𝑦)))
8773, 81, 863eqtr3d 2801 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘((1st𝐺)‘𝑥))‘𝑦)))
8887mpteq2dva 5127 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)((Id‘𝐷)‘𝑦))) = (𝑦 ∈ (Base‘𝐷) ↦ ((Id‘𝐸)‘((1st ‘((1st𝐺)‘𝑥))‘𝑦))))
8930adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐸 ∈ Cat)
90 eqid 2758 . . . . . . . . . 10 (Base‘𝐸) = (Base‘𝐸)
9190, 66cidfn 17008 . . . . . . . . 9 (𝐸 ∈ Cat → (Id‘𝐸) Fn (Base‘𝐸))
9289, 91syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → (Id‘𝐸) Fn (Base‘𝐸))
93 dffn2 6500 . . . . . . . 8 ((Id‘𝐸) Fn (Base‘𝐸) ↔ (Id‘𝐸):(Base‘𝐸)⟶V)
9492, 93sylib 221 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → (Id‘𝐸):(Base‘𝐸)⟶V)
95 relfunc 17191 . . . . . . . . 9 Rel (𝐷 Func 𝐸)
96 1st2ndbr 7745 . . . . . . . . 9 ((Rel (𝐷 Func 𝐸) ∧ ((1st𝐺)‘𝑥) ∈ (𝐷 Func 𝐸)) → (1st ‘((1st𝐺)‘𝑥))(𝐷 Func 𝐸)(2nd ‘((1st𝐺)‘𝑥)))
9795, 39, 96sylancr 590 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st ‘((1st𝐺)‘𝑥))(𝐷 Func 𝐸)(2nd ‘((1st𝐺)‘𝑥)))
986, 90, 97funcf1 17195 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st ‘((1st𝐺)‘𝑥)):(Base‘𝐷)⟶(Base‘𝐸))
99 fcompt 6886 . . . . . . 7 (((Id‘𝐸):(Base‘𝐸)⟶V ∧ (1st ‘((1st𝐺)‘𝑥)):(Base‘𝐷)⟶(Base‘𝐸)) → ((Id‘𝐸) ∘ (1st ‘((1st𝐺)‘𝑥))) = (𝑦 ∈ (Base‘𝐷) ↦ ((Id‘𝐸)‘((1st ‘((1st𝐺)‘𝑥))‘𝑦))))
10094, 98, 99syl2anc 587 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸) ∘ (1st ‘((1st𝐺)‘𝑥))) = (𝑦 ∈ (Base‘𝐷) ↦ ((Id‘𝐸)‘((1st ‘((1st𝐺)‘𝑥))‘𝑦))))
10188, 100eqtr4d 2796 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)((Id‘𝐷)‘𝑦))) = ((Id‘𝐸) ∘ (1st ‘((1st𝐺)‘𝑥))))
1022, 9, 8, 34, 37catidcl 17011 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
103 eqid 2758 . . . . . 6 ((𝑥(2nd𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((𝑥(2nd𝐺)𝑥)‘((Id‘𝐶)‘𝑥))
1041, 2, 34, 35, 36, 6, 9, 10, 37, 37, 102, 103curf2 17545 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = (𝑦 ∈ (Base‘𝐷) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑦⟩)((Id‘𝐷)‘𝑦))))
10521, 25, 66, 39fucid 17300 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑄)‘((1st𝐺)‘𝑥)) = ((Id‘𝐸) ∘ (1st ‘((1st𝐺)‘𝑥))))
106101, 104, 1053eqtr4d 2803 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝑄)‘((1st𝐺)‘𝑥)))
10733ad2ant1 1130 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐶 ∈ Cat)
108107adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝐶 ∈ Cat)
10943ad2ant1 1130 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐷 ∈ Cat)
110109adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat)
11153ad2ant1 1130 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
112111adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
113 simp21 1203 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ (Base‘𝐶))
114113adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑥 ∈ (Base‘𝐶))
115 simpr 488 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑤 ∈ (Base‘𝐷))
1161, 2, 108, 110, 112, 6, 114, 38, 115curf11 17542 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st ‘((1st𝐺)‘𝑥))‘𝑤) = (𝑥(1st𝐹)𝑤))
117 df-ov 7153 . . . . . . . . . . 11 (𝑥(1st𝐹)𝑤) = ((1st𝐹)‘⟨𝑥, 𝑤⟩)
118116, 117eqtrdi 2809 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st ‘((1st𝐺)‘𝑥))‘𝑤) = ((1st𝐹)‘⟨𝑥, 𝑤⟩))
119 simp22 1204 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ (Base‘𝐶))
120119adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑦 ∈ (Base‘𝐶))
121 eqid 2758 . . . . . . . . . . . 12 ((1st𝐺)‘𝑦) = ((1st𝐺)‘𝑦)
1221, 2, 108, 110, 112, 6, 120, 121, 115curf11 17542 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st ‘((1st𝐺)‘𝑦))‘𝑤) = (𝑦(1st𝐹)𝑤))
123 df-ov 7153 . . . . . . . . . . 11 (𝑦(1st𝐹)𝑤) = ((1st𝐹)‘⟨𝑦, 𝑤⟩)
124122, 123eqtrdi 2809 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st ‘((1st𝐺)‘𝑦))‘𝑤) = ((1st𝐹)‘⟨𝑦, 𝑤⟩))
125118, 124opeq12d 4771 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨((1st ‘((1st𝐺)‘𝑥))‘𝑤), ((1st ‘((1st𝐺)‘𝑦))‘𝑤)⟩ = ⟨((1st𝐹)‘⟨𝑥, 𝑤⟩), ((1st𝐹)‘⟨𝑦, 𝑤⟩)⟩)
126 simp23 1205 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶))
127126adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑧 ∈ (Base‘𝐶))
128 eqid 2758 . . . . . . . . . . 11 ((1st𝐺)‘𝑧) = ((1st𝐺)‘𝑧)
1291, 2, 108, 110, 112, 6, 127, 128, 115curf11 17542 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st ‘((1st𝐺)‘𝑧))‘𝑤) = (𝑧(1st𝐹)𝑤))
130 df-ov 7153 . . . . . . . . . 10 (𝑧(1st𝐹)𝑤) = ((1st𝐹)‘⟨𝑧, 𝑤⟩)
131129, 130eqtrdi 2809 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st ‘((1st𝐺)‘𝑧))‘𝑤) = ((1st𝐹)‘⟨𝑧, 𝑤⟩))
132125, 131oveq12d 7168 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (⟨((1st ‘((1st𝐺)‘𝑥))‘𝑤), ((1st ‘((1st𝐺)‘𝑦))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑧))‘𝑤)) = (⟨((1st𝐹)‘⟨𝑥, 𝑤⟩), ((1st𝐹)‘⟨𝑦, 𝑤⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑧, 𝑤⟩)))
133 simp3r 1199 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
134133adantr 484 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
135 eqid 2758 . . . . . . . . . 10 ((𝑦(2nd𝐺)𝑧)‘𝑔) = ((𝑦(2nd𝐺)𝑧)‘𝑔)
1361, 2, 108, 110, 112, 6, 9, 10, 120, 127, 134, 135, 115curf2val 17546 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((𝑦(2nd𝐺)𝑧)‘𝑔)‘𝑤) = (𝑔(⟨𝑦, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)((Id‘𝐷)‘𝑤)))
137 df-ov 7153 . . . . . . . . 9 (𝑔(⟨𝑦, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)((Id‘𝐷)‘𝑤)) = ((⟨𝑦, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)‘⟨𝑔, ((Id‘𝐷)‘𝑤)⟩)
138136, 137eqtrdi 2809 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((𝑦(2nd𝐺)𝑧)‘𝑔)‘𝑤) = ((⟨𝑦, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)‘⟨𝑔, ((Id‘𝐷)‘𝑤)⟩))
139 simp3l 1198 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
140139adantr 484 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
141 eqid 2758 . . . . . . . . . 10 ((𝑥(2nd𝐺)𝑦)‘𝑓) = ((𝑥(2nd𝐺)𝑦)‘𝑓)
1421, 2, 108, 110, 112, 6, 9, 10, 114, 120, 140, 141, 115curf2val 17546 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((𝑥(2nd𝐺)𝑦)‘𝑓)‘𝑤) = (𝑓(⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑦, 𝑤⟩)((Id‘𝐷)‘𝑤)))
143 df-ov 7153 . . . . . . . . 9 (𝑓(⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑦, 𝑤⟩)((Id‘𝐷)‘𝑤)) = ((⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑦, 𝑤⟩)‘⟨𝑓, ((Id‘𝐷)‘𝑤)⟩)
144142, 143eqtrdi 2809 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((𝑥(2nd𝐺)𝑦)‘𝑓)‘𝑤) = ((⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑦, 𝑤⟩)‘⟨𝑓, ((Id‘𝐷)‘𝑤)⟩))
145132, 138, 144oveq123d 7171 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((((𝑦(2nd𝐺)𝑧)‘𝑔)‘𝑤)(⟨((1st ‘((1st𝐺)‘𝑥))‘𝑤), ((1st ‘((1st𝐺)‘𝑦))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑧))‘𝑤))(((𝑥(2nd𝐺)𝑦)‘𝑓)‘𝑤)) = (((⟨𝑦, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)‘⟨𝑔, ((Id‘𝐷)‘𝑤)⟩)(⟨((1st𝐹)‘⟨𝑥, 𝑤⟩), ((1st𝐹)‘⟨𝑦, 𝑤⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑧, 𝑤⟩))((⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑦, 𝑤⟩)‘⟨𝑓, ((Id‘𝐷)‘𝑤)⟩)))
146 eqid 2758 . . . . . . . 8 (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
147 eqid 2758 . . . . . . . 8 (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
148 eqid 2758 . . . . . . . 8 (comp‘𝐸) = (comp‘𝐸)
14967, 112, 68sylancr 590 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
150 opelxpi 5561 . . . . . . . . 9 ((𝑥 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑤⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
151113, 150sylan 583 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑤⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
152 opelxpi 5561 . . . . . . . . 9 ((𝑦 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑦, 𝑤⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
153119, 152sylan 583 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑦, 𝑤⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
154 opelxpi 5561 . . . . . . . . 9 ((𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑧, 𝑤⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
155126, 154sylan 583 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑧, 𝑤⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
1566, 7, 10, 110, 115catidcl 17011 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((Id‘𝐷)‘𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤))
157140, 156opelxpd 5562 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑓, ((Id‘𝐷)‘𝑤)⟩ ∈ ((𝑥(Hom ‘𝐶)𝑦) × (𝑤(Hom ‘𝐷)𝑤)))
15863, 2, 6, 9, 7, 114, 115, 120, 115, 146xpchom2 17502 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (⟨𝑥, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑤⟩) = ((𝑥(Hom ‘𝐶)𝑦) × (𝑤(Hom ‘𝐷)𝑤)))
159157, 158eleqtrrd 2855 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑓, ((Id‘𝐷)‘𝑤)⟩ ∈ (⟨𝑥, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑤⟩))
160134, 156opelxpd 5562 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑔, ((Id‘𝐷)‘𝑤)⟩ ∈ ((𝑦(Hom ‘𝐶)𝑧) × (𝑤(Hom ‘𝐷)𝑤)))
16163, 2, 6, 9, 7, 120, 115, 127, 115, 146xpchom2 17502 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (⟨𝑦, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑧, 𝑤⟩) = ((𝑦(Hom ‘𝐶)𝑧) × (𝑤(Hom ‘𝐷)𝑤)))
162160, 161eleqtrrd 2855 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨𝑔, ((Id‘𝐷)‘𝑤)⟩ ∈ (⟨𝑦, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑧, 𝑤⟩))
16364, 146, 147, 148, 149, 151, 153, 155, 159, 162funcco 17200 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)‘(⟨𝑔, ((Id‘𝐷)‘𝑤)⟩(⟨⟨𝑥, 𝑤⟩, ⟨𝑦, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑧, 𝑤⟩)⟨𝑓, ((Id‘𝐷)‘𝑤)⟩)) = (((⟨𝑦, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)‘⟨𝑔, ((Id‘𝐷)‘𝑤)⟩)(⟨((1st𝐹)‘⟨𝑥, 𝑤⟩), ((1st𝐹)‘⟨𝑦, 𝑤⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑧, 𝑤⟩))((⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑦, 𝑤⟩)‘⟨𝑓, ((Id‘𝐷)‘𝑤)⟩)))
164 eqid 2758 . . . . . . . . . . 11 (comp‘𝐷) = (comp‘𝐷)
16563, 2, 6, 9, 7, 114, 115, 120, 115, 26, 164, 147, 127, 115, 140, 156, 134, 156xpcco2 17503 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (⟨𝑔, ((Id‘𝐷)‘𝑤)⟩(⟨⟨𝑥, 𝑤⟩, ⟨𝑦, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑧, 𝑤⟩)⟨𝑓, ((Id‘𝐷)‘𝑤)⟩) = ⟨(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓), (((Id‘𝐷)‘𝑤)(⟨𝑤, 𝑤⟩(comp‘𝐷)𝑤)((Id‘𝐷)‘𝑤))⟩)
1666, 7, 10, 110, 115, 164, 115, 156catlid 17012 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((Id‘𝐷)‘𝑤)(⟨𝑤, 𝑤⟩(comp‘𝐷)𝑤)((Id‘𝐷)‘𝑤)) = ((Id‘𝐷)‘𝑤))
167166opeq2d 4770 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ⟨(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓), (((Id‘𝐷)‘𝑤)(⟨𝑤, 𝑤⟩(comp‘𝐷)𝑤)((Id‘𝐷)‘𝑤))⟩ = ⟨(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓), ((Id‘𝐷)‘𝑤)⟩)
168165, 167eqtrd 2793 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (⟨𝑔, ((Id‘𝐷)‘𝑤)⟩(⟨⟨𝑥, 𝑤⟩, ⟨𝑦, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑧, 𝑤⟩)⟨𝑓, ((Id‘𝐷)‘𝑤)⟩) = ⟨(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓), ((Id‘𝐷)‘𝑤)⟩)
169168fveq2d 6662 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)‘(⟨𝑔, ((Id‘𝐷)‘𝑤)⟩(⟨⟨𝑥, 𝑤⟩, ⟨𝑦, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑧, 𝑤⟩)⟨𝑓, ((Id‘𝐷)‘𝑤)⟩)) = ((⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)‘⟨(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓), ((Id‘𝐷)‘𝑤)⟩))
170 df-ov 7153 . . . . . . . 8 ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)(⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)((Id‘𝐷)‘𝑤)) = ((⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)‘⟨(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓), ((Id‘𝐷)‘𝑤)⟩)
171169, 170eqtr4di 2811 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)‘(⟨𝑔, ((Id‘𝐷)‘𝑤)⟩(⟨⟨𝑥, 𝑤⟩, ⟨𝑦, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑧, 𝑤⟩)⟨𝑓, ((Id‘𝐷)‘𝑤)⟩)) = ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)(⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)((Id‘𝐷)‘𝑤)))
172145, 163, 1713eqtr2rd 2800 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)(⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)((Id‘𝐷)‘𝑤)) = ((((𝑦(2nd𝐺)𝑧)‘𝑔)‘𝑤)(⟨((1st ‘((1st𝐺)‘𝑥))‘𝑤), ((1st ‘((1st𝐺)‘𝑦))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑧))‘𝑤))(((𝑥(2nd𝐺)𝑦)‘𝑓)‘𝑤)))
173172mpteq2dva 5127 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑤 ∈ (Base‘𝐷) ↦ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)(⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)((Id‘𝐷)‘𝑤))) = (𝑤 ∈ (Base‘𝐷) ↦ ((((𝑦(2nd𝐺)𝑧)‘𝑔)‘𝑤)(⟨((1st ‘((1st𝐺)‘𝑥))‘𝑤), ((1st ‘((1st𝐺)‘𝑦))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑧))‘𝑤))(((𝑥(2nd𝐺)𝑦)‘𝑓)‘𝑤))))
1742, 9, 26, 107, 113, 119, 126, 139, 133catcocl 17014 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
175 eqid 2758 . . . . . 6 ((𝑥(2nd𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((𝑥(2nd𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
1761, 2, 107, 109, 111, 6, 9, 10, 113, 126, 174, 175curf2 17545 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (𝑤 ∈ (Base‘𝐷) ↦ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)(⟨𝑥, 𝑤⟩(2nd𝐹)⟨𝑧, 𝑤⟩)((Id‘𝐷)‘𝑤))))
1771, 2, 107, 109, 111, 6, 9, 10, 113, 119, 139, 141, 23curf2cl 17547 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝐺)𝑦)‘𝑓) ∈ (((1st𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st𝐺)‘𝑦)))
1781, 2, 107, 109, 111, 6, 9, 10, 119, 126, 133, 135, 23curf2cl 17547 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd𝐺)𝑧)‘𝑔) ∈ (((1st𝐺)‘𝑦)(𝐷 Nat 𝐸)((1st𝐺)‘𝑧)))
17921, 23, 6, 148, 27, 177, 178fucco 17291 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd𝐺)𝑧)‘𝑔)(⟨((1st𝐺)‘𝑥), ((1st𝐺)‘𝑦)⟩(comp‘𝑄)((1st𝐺)‘𝑧))((𝑥(2nd𝐺)𝑦)‘𝑓)) = (𝑤 ∈ (Base‘𝐷) ↦ ((((𝑦(2nd𝐺)𝑧)‘𝑔)‘𝑤)(⟨((1st ‘((1st𝐺)‘𝑥))‘𝑤), ((1st ‘((1st𝐺)‘𝑦))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑧))‘𝑤))(((𝑥(2nd𝐺)𝑦)‘𝑓)‘𝑤))))
180173, 176, 1793eqtr4d 2803 . . . 4 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐺)𝑧)‘𝑔)(⟨((1st𝐺)‘𝑥), ((1st𝐺)‘𝑦)⟩(comp‘𝑄)((1st𝐺)‘𝑧))((𝑥(2nd𝐺)𝑦)‘𝑓)))
1812, 22, 9, 24, 8, 25, 26, 27, 3, 31, 40, 46, 62, 106, 180isfuncd 17194 . . 3 (𝜑 → (1st𝐺)(𝐶 Func 𝑄)(2nd𝐺))
182 df-br 5033 . . 3 ((1st𝐺)(𝐶 Func 𝑄)(2nd𝐺) ↔ ⟨(1st𝐺), (2nd𝐺)⟩ ∈ (𝐶 Func 𝑄))
183181, 182sylib 221 . 2 (𝜑 → ⟨(1st𝐺), (2nd𝐺)⟩ ∈ (𝐶 Func 𝑄))
18420, 183eqeltrd 2852 1 (𝜑𝐺 ∈ (𝐶 Func 𝑄))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  Vcvv 3409  ⟨cop 4528   class class class wbr 5032   ↦ cmpt 5112   × cxp 5522   ∘ ccom 5528  Rel wrel 5529   Fn wfn 6330  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150   ∈ cmpo 7152  1st c1st 7691  2nd c2nd 7692  Basecbs 16541  Hom chom 16634  compcco 16635  Catccat 16993  Idccid 16994   Func cfunc 17183   Nat cnat 17270   FuncCat cfuc 17271   ×c cxpc 17484   curryF ccurf 17526 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-er 8299  df-map 8418  df-ixp 8480  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-nn 11675  df-2 11737  df-3 11738  df-4 11739  df-5 11740  df-6 11741  df-7 11742  df-8 11743  df-9 11744  df-n0 11935  df-z 12021  df-dec 12138  df-uz 12283  df-fz 12940  df-struct 16543  df-ndx 16544  df-slot 16545  df-base 16547  df-hom 16647  df-cco 16648  df-cat 16997  df-cid 16998  df-func 17187  df-nat 17272  df-fuc 17273  df-xpc 17488  df-curf 17530 This theorem is referenced by:  uncfcurf  17555  diagcl  17557  curf2ndf  17563  yoncl  17578
 Copyright terms: Public domain W3C validator