| Step | Hyp | Ref
| Expression |
| 1 | | curfcl.g |
. . . 4
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 3 | | curfcl.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 4 | | curfcl.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 5 | | curfcl.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
| 6 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 7 | | eqid 2737 |
. . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 8 | | eqid 2737 |
. . . 4
⊢
(Id‘𝐶) =
(Id‘𝐶) |
| 9 | | eqid 2737 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 10 | | eqid 2737 |
. . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) |
| 11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | curfval 18268 |
. . 3
⊢ (𝜑 → 𝐺 = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))〉) |
| 12 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
| 13 | 12 | mptex 7243 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉) ∈ V |
| 14 | 12, 12 | mpoex 8104 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) ∈ V |
| 15 | 13, 14 | op1std 8024 |
. . . . 5
⊢ (𝐺 = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))〉 → (1st
‘𝐺) = (𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉)) |
| 16 | 11, 15 | syl 17 |
. . . 4
⊢ (𝜑 → (1st
‘𝐺) = (𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉)) |
| 17 | 13, 14 | op2ndd 8025 |
. . . . 5
⊢ (𝐺 = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))〉 → (2nd
‘𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))) |
| 18 | 11, 17 | syl 17 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))) |
| 19 | 16, 18 | opeq12d 4881 |
. . 3
⊢ (𝜑 → 〈(1st
‘𝐺), (2nd
‘𝐺)〉 =
〈(𝑥 ∈
(Base‘𝐶) ↦
〈(𝑦 ∈
(Base‘𝐷) ↦
(𝑥(1st
‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))〉) |
| 20 | 11, 19 | eqtr4d 2780 |
. 2
⊢ (𝜑 → 𝐺 = 〈(1st ‘𝐺), (2nd ‘𝐺)〉) |
| 21 | | curfcl.q |
. . . . 5
⊢ 𝑄 = (𝐷 FuncCat 𝐸) |
| 22 | 21 | fucbas 18008 |
. . . 4
⊢ (𝐷 Func 𝐸) = (Base‘𝑄) |
| 23 | | eqid 2737 |
. . . . 5
⊢ (𝐷 Nat 𝐸) = (𝐷 Nat 𝐸) |
| 24 | 21, 23 | fuchom 18009 |
. . . 4
⊢ (𝐷 Nat 𝐸) = (Hom ‘𝑄) |
| 25 | | eqid 2737 |
. . . 4
⊢
(Id‘𝑄) =
(Id‘𝑄) |
| 26 | | eqid 2737 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 27 | | eqid 2737 |
. . . 4
⊢
(comp‘𝑄) =
(comp‘𝑄) |
| 28 | | funcrcl 17908 |
. . . . . . 7
⊢ (𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸) → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat)) |
| 29 | 5, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat)) |
| 30 | 29 | simprd 495 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ Cat) |
| 31 | 21, 4, 30 | fuccat 18018 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ Cat) |
| 32 | | opex 5469 |
. . . . . 6
⊢
〈(𝑦 ∈
(Base‘𝐷) ↦
(𝑥(1st
‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉 ∈ V |
| 33 | 32 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉 ∈ V) |
| 34 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat) |
| 35 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat) |
| 36 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
| 37 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
| 38 | | eqid 2737 |
. . . . . 6
⊢
((1st ‘𝐺)‘𝑥) = ((1st ‘𝐺)‘𝑥) |
| 39 | 1, 2, 34, 35, 36, 6, 37, 38 | curf1cl 18273 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (𝐷 Func 𝐸)) |
| 40 | 33, 16, 39 | fmpt2d 7144 |
. . . 4
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐶)⟶(𝐷 Func 𝐸)) |
| 41 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) |
| 42 | | ovex 7464 |
. . . . . . 7
⊢ (𝑥(Hom ‘𝐶)𝑦) ∈ V |
| 43 | 42 | mptex 7243 |
. . . . . 6
⊢ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))) ∈ V |
| 44 | 41, 43 | fnmpoi 8095 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) Fn ((Base‘𝐶) × (Base‘𝐶)) |
| 45 | 18 | fneq1d 6661 |
. . . . 5
⊢ (𝜑 → ((2nd
‘𝐺) Fn
((Base‘𝐶) ×
(Base‘𝐶)) ↔
(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) Fn ((Base‘𝐶) × (Base‘𝐶)))) |
| 46 | 44, 45 | mpbiri 258 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐺) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |
| 47 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝐷)
∈ V |
| 48 | 47 | mptex 7243 |
. . . . . 6
⊢ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))) ∈ V |
| 49 | 48 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))) ∈ V) |
| 50 | 18 | oveqd 7448 |
. . . . . 6
⊢ (𝜑 → (𝑥(2nd ‘𝐺)𝑦) = (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))𝑦)) |
| 51 | 41 | ovmpt4g 7580 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))) ∈ V) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))𝑦) = (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) |
| 52 | 43, 51 | mp3an3 1452 |
. . . . . 6
⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))𝑦) = (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) |
| 53 | 50, 52 | sylan9eq 2797 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦) = (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) |
| 54 | 3 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐶 ∈ Cat) |
| 55 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐷 ∈ Cat) |
| 56 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
| 57 | | simplrl 777 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶)) |
| 58 | | simplrr 778 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶)) |
| 59 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
| 60 | | eqid 2737 |
. . . . . 6
⊢ ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) = ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) |
| 61 | 1, 2, 54, 55, 56, 6, 9, 10, 57, 58, 59, 60, 23 | curf2cl 18276 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) ∈ (((1st ‘𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑦))) |
| 62 | 49, 53, 61 | fmpt2d 7144 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑦))) |
| 63 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
| 64 | 63, 2, 6 | xpcbas 18223 |
. . . . . . . . 9
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
(Base‘(𝐶
×c 𝐷)) |
| 65 | | eqid 2737 |
. . . . . . . . 9
⊢
(Id‘(𝐶
×c 𝐷)) = (Id‘(𝐶 ×c 𝐷)) |
| 66 | | eqid 2737 |
. . . . . . . . 9
⊢
(Id‘𝐸) =
(Id‘𝐸) |
| 67 | | relfunc 17907 |
. . . . . . . . . . 11
⊢ Rel
((𝐶
×c 𝐷) Func 𝐸) |
| 68 | | 1st2ndbr 8067 |
. . . . . . . . . . 11
⊢ ((Rel
((𝐶
×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
| 69 | 67, 5, 68 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐹)((𝐶 ×c
𝐷) Func 𝐸)(2nd ‘𝐹)) |
| 70 | 69 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
| 71 | | opelxpi 5722 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐷)) → 〈𝑥, 𝑦〉 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
| 72 | 71 | adantll 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 〈𝑥, 𝑦〉 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
| 73 | 64, 65, 66, 70, 72 | funcid 17915 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)‘((Id‘(𝐶 ×c 𝐷))‘〈𝑥, 𝑦〉)) = ((Id‘𝐸)‘((1st ‘𝐹)‘〈𝑥, 𝑦〉))) |
| 74 | 3 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐶 ∈ Cat) |
| 75 | 4 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat) |
| 76 | 37 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝑥 ∈ (Base‘𝐶)) |
| 77 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝑦 ∈ (Base‘𝐷)) |
| 78 | 63, 74, 75, 2, 6, 8,
10, 65, 76, 77 | xpcid 18234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((Id‘(𝐶 ×c 𝐷))‘〈𝑥, 𝑦〉) = 〈((Id‘𝐶)‘𝑥), ((Id‘𝐷)‘𝑦)〉) |
| 79 | 78 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)‘((Id‘(𝐶 ×c 𝐷))‘〈𝑥, 𝑦〉)) = ((〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)‘〈((Id‘𝐶)‘𝑥), ((Id‘𝐷)‘𝑦)〉)) |
| 80 | | df-ov 7434 |
. . . . . . . . 9
⊢
(((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)((Id‘𝐷)‘𝑦)) = ((〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)‘〈((Id‘𝐶)‘𝑥), ((Id‘𝐷)‘𝑦)〉) |
| 81 | 79, 80 | eqtr4di 2795 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)‘((Id‘(𝐶 ×c 𝐷))‘〈𝑥, 𝑦〉)) = (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)((Id‘𝐷)‘𝑦))) |
| 82 | 5 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
| 83 | 1, 2, 74, 75, 82, 6, 76, 38, 77 | curf11 18271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦) = (𝑥(1st ‘𝐹)𝑦)) |
| 84 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑥(1st ‘𝐹)𝑦) = ((1st ‘𝐹)‘〈𝑥, 𝑦〉) |
| 85 | 83, 84 | eqtr2di 2794 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st ‘𝐹)‘〈𝑥, 𝑦〉) = ((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦)) |
| 86 | 85 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((Id‘𝐸)‘((1st ‘𝐹)‘〈𝑥, 𝑦〉)) = ((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦))) |
| 87 | 73, 81, 86 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦))) |
| 88 | 87 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)((Id‘𝐷)‘𝑦))) = (𝑦 ∈ (Base‘𝐷) ↦ ((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦)))) |
| 89 | 30 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐸 ∈ Cat) |
| 90 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐸) =
(Base‘𝐸) |
| 91 | 90, 66 | cidfn 17722 |
. . . . . . . . 9
⊢ (𝐸 ∈ Cat →
(Id‘𝐸) Fn
(Base‘𝐸)) |
| 92 | 89, 91 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Id‘𝐸) Fn (Base‘𝐸)) |
| 93 | | dffn2 6738 |
. . . . . . . 8
⊢
((Id‘𝐸) Fn
(Base‘𝐸) ↔
(Id‘𝐸):(Base‘𝐸)⟶V) |
| 94 | 92, 93 | sylib 218 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Id‘𝐸):(Base‘𝐸)⟶V) |
| 95 | | relfunc 17907 |
. . . . . . . . 9
⊢ Rel
(𝐷 Func 𝐸) |
| 96 | | 1st2ndbr 8067 |
. . . . . . . . 9
⊢ ((Rel
(𝐷 Func 𝐸) ∧ ((1st ‘𝐺)‘𝑥) ∈ (𝐷 Func 𝐸)) → (1st
‘((1st ‘𝐺)‘𝑥))(𝐷 Func 𝐸)(2nd ‘((1st
‘𝐺)‘𝑥))) |
| 97 | 95, 39, 96 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st
‘((1st ‘𝐺)‘𝑥))(𝐷 Func 𝐸)(2nd ‘((1st
‘𝐺)‘𝑥))) |
| 98 | 6, 90, 97 | funcf1 17911 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st
‘((1st ‘𝐺)‘𝑥)):(Base‘𝐷)⟶(Base‘𝐸)) |
| 99 | | fcompt 7153 |
. . . . . . 7
⊢
(((Id‘𝐸):(Base‘𝐸)⟶V ∧ (1st
‘((1st ‘𝐺)‘𝑥)):(Base‘𝐷)⟶(Base‘𝐸)) → ((Id‘𝐸) ∘ (1st
‘((1st ‘𝐺)‘𝑥))) = (𝑦 ∈ (Base‘𝐷) ↦ ((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦)))) |
| 100 | 94, 98, 99 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸) ∘ (1st
‘((1st ‘𝐺)‘𝑥))) = (𝑦 ∈ (Base‘𝐷) ↦ ((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦)))) |
| 101 | 88, 100 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)((Id‘𝐷)‘𝑦))) = ((Id‘𝐸) ∘ (1st
‘((1st ‘𝐺)‘𝑥)))) |
| 102 | 2, 9, 8, 34, 37 | catidcl 17725 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥)) |
| 103 | | eqid 2737 |
. . . . . 6
⊢ ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) |
| 104 | 1, 2, 34, 35, 36, 6, 9, 10, 37, 37, 102, 103 | curf2 18274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = (𝑦 ∈ (Base‘𝐷) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑦〉)((Id‘𝐷)‘𝑦)))) |
| 105 | 21, 25, 66, 39 | fucid 18019 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑄)‘((1st ‘𝐺)‘𝑥)) = ((Id‘𝐸) ∘ (1st
‘((1st ‘𝐺)‘𝑥)))) |
| 106 | 101, 104,
105 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝑄)‘((1st ‘𝐺)‘𝑥))) |
| 107 | 3 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐶 ∈ Cat) |
| 108 | 107 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝐶 ∈ Cat) |
| 109 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐷 ∈ Cat) |
| 110 | 109 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat) |
| 111 | 5 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
| 112 | 111 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
| 113 | | simp21 1207 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ (Base‘𝐶)) |
| 114 | 113 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑥 ∈ (Base‘𝐶)) |
| 115 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑤 ∈ (Base‘𝐷)) |
| 116 | 1, 2, 108, 110, 112, 6, 114, 38, 115 | curf11 18271 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st
‘((1st ‘𝐺)‘𝑥))‘𝑤) = (𝑥(1st ‘𝐹)𝑤)) |
| 117 | | df-ov 7434 |
. . . . . . . . . . 11
⊢ (𝑥(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘〈𝑥, 𝑤〉) |
| 118 | 116, 117 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st
‘((1st ‘𝐺)‘𝑥))‘𝑤) = ((1st ‘𝐹)‘〈𝑥, 𝑤〉)) |
| 119 | | simp22 1208 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ (Base‘𝐶)) |
| 120 | 119 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑦 ∈ (Base‘𝐶)) |
| 121 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
((1st ‘𝐺)‘𝑦) = ((1st ‘𝐺)‘𝑦) |
| 122 | 1, 2, 108, 110, 112, 6, 120, 121, 115 | curf11 18271 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st
‘((1st ‘𝐺)‘𝑦))‘𝑤) = (𝑦(1st ‘𝐹)𝑤)) |
| 123 | | df-ov 7434 |
. . . . . . . . . . 11
⊢ (𝑦(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘〈𝑦, 𝑤〉) |
| 124 | 122, 123 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st
‘((1st ‘𝐺)‘𝑦))‘𝑤) = ((1st ‘𝐹)‘〈𝑦, 𝑤〉)) |
| 125 | 118, 124 | opeq12d 4881 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑤), ((1st ‘((1st
‘𝐺)‘𝑦))‘𝑤)〉 = 〈((1st ‘𝐹)‘〈𝑥, 𝑤〉), ((1st ‘𝐹)‘〈𝑦, 𝑤〉)〉) |
| 126 | | simp23 1209 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶)) |
| 127 | 126 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑧 ∈ (Base‘𝐶)) |
| 128 | | eqid 2737 |
. . . . . . . . . . 11
⊢
((1st ‘𝐺)‘𝑧) = ((1st ‘𝐺)‘𝑧) |
| 129 | 1, 2, 108, 110, 112, 6, 127, 128, 115 | curf11 18271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st
‘((1st ‘𝐺)‘𝑧))‘𝑤) = (𝑧(1st ‘𝐹)𝑤)) |
| 130 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑧(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘〈𝑧, 𝑤〉) |
| 131 | 129, 130 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((1st
‘((1st ‘𝐺)‘𝑧))‘𝑤) = ((1st ‘𝐹)‘〈𝑧, 𝑤〉)) |
| 132 | 125, 131 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑤), ((1st ‘((1st
‘𝐺)‘𝑦))‘𝑤)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑧))‘𝑤)) = (〈((1st ‘𝐹)‘〈𝑥, 𝑤〉), ((1st ‘𝐹)‘〈𝑦, 𝑤〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑧, 𝑤〉))) |
| 133 | | simp3r 1203 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) |
| 134 | 133 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) |
| 135 | | eqid 2737 |
. . . . . . . . . 10
⊢ ((𝑦(2nd ‘𝐺)𝑧)‘𝑔) = ((𝑦(2nd ‘𝐺)𝑧)‘𝑔) |
| 136 | 1, 2, 108, 110, 112, 6, 9, 10, 120, 127, 134, 135, 115 | curf2val 18275 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)‘𝑤) = (𝑔(〈𝑦, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)((Id‘𝐷)‘𝑤))) |
| 137 | | df-ov 7434 |
. . . . . . . . 9
⊢ (𝑔(〈𝑦, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)((Id‘𝐷)‘𝑤)) = ((〈𝑦, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)‘〈𝑔, ((Id‘𝐷)‘𝑤)〉) |
| 138 | 136, 137 | eqtrdi 2793 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)‘𝑤) = ((〈𝑦, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)‘〈𝑔, ((Id‘𝐷)‘𝑤)〉)) |
| 139 | | simp3l 1202 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
| 140 | 139 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
| 141 | | eqid 2737 |
. . . . . . . . . 10
⊢ ((𝑥(2nd ‘𝐺)𝑦)‘𝑓) = ((𝑥(2nd ‘𝐺)𝑦)‘𝑓) |
| 142 | 1, 2, 108, 110, 112, 6, 9, 10, 114, 120, 140, 141, 115 | curf2val 18275 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((𝑥(2nd ‘𝐺)𝑦)‘𝑓)‘𝑤) = (𝑓(〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑦, 𝑤〉)((Id‘𝐷)‘𝑤))) |
| 143 | | df-ov 7434 |
. . . . . . . . 9
⊢ (𝑓(〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑦, 𝑤〉)((Id‘𝐷)‘𝑤)) = ((〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑦, 𝑤〉)‘〈𝑓, ((Id‘𝐷)‘𝑤)〉) |
| 144 | 142, 143 | eqtrdi 2793 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((𝑥(2nd ‘𝐺)𝑦)‘𝑓)‘𝑤) = ((〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑦, 𝑤〉)‘〈𝑓, ((Id‘𝐷)‘𝑤)〉)) |
| 145 | 132, 138,
144 | oveq123d 7452 |
. . . . . . 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 2737 |
. . . . . . . 8
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
| 147 | | eqid 2737 |
. . . . . . . 8
⊢
(comp‘(𝐶
×c 𝐷)) = (comp‘(𝐶 ×c 𝐷)) |
| 148 | | eqid 2737 |
. . . . . . . 8
⊢
(comp‘𝐸) =
(comp‘𝐸) |
| 149 | 67, 112, 68 | sylancr 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
| 150 | | opelxpi 5722 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑥, 𝑤〉 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
| 151 | 113, 150 | sylan 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑥, 𝑤〉 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
| 152 | | opelxpi 5722 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑦, 𝑤〉 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
| 153 | 119, 152 | sylan 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑦, 𝑤〉 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
| 154 | | opelxpi 5722 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑧, 𝑤〉 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
| 155 | 126, 154 | sylan 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑧, 𝑤〉 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
| 156 | 6, 7, 10, 110, 115 | catidcl 17725 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((Id‘𝐷)‘𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤)) |
| 157 | 140, 156 | opelxpd 5724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑓, ((Id‘𝐷)‘𝑤)〉 ∈ ((𝑥(Hom ‘𝐶)𝑦) × (𝑤(Hom ‘𝐷)𝑤))) |
| 158 | 63, 2, 6, 9, 7, 114, 115, 120, 115, 146 | xpchom2 18231 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (〈𝑥, 𝑤〉(Hom ‘(𝐶 ×c 𝐷))〈𝑦, 𝑤〉) = ((𝑥(Hom ‘𝐶)𝑦) × (𝑤(Hom ‘𝐷)𝑤))) |
| 159 | 157, 158 | eleqtrrd 2844 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑓, ((Id‘𝐷)‘𝑤)〉 ∈ (〈𝑥, 𝑤〉(Hom ‘(𝐶 ×c 𝐷))〈𝑦, 𝑤〉)) |
| 160 | 134, 156 | opelxpd 5724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑔, ((Id‘𝐷)‘𝑤)〉 ∈ ((𝑦(Hom ‘𝐶)𝑧) × (𝑤(Hom ‘𝐷)𝑤))) |
| 161 | 63, 2, 6, 9, 7, 120, 115, 127, 115, 146 | xpchom2 18231 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (〈𝑦, 𝑤〉(Hom ‘(𝐶 ×c 𝐷))〈𝑧, 𝑤〉) = ((𝑦(Hom ‘𝐶)𝑧) × (𝑤(Hom ‘𝐷)𝑤))) |
| 162 | 160, 161 | eleqtrrd 2844 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈𝑔, ((Id‘𝐷)‘𝑤)〉 ∈ (〈𝑦, 𝑤〉(Hom ‘(𝐶 ×c 𝐷))〈𝑧, 𝑤〉)) |
| 163 | 64, 146, 147, 148, 149, 151, 153, 155, 159, 162 | funcco 17916 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)‘(〈𝑔, ((Id‘𝐷)‘𝑤)〉(〈〈𝑥, 𝑤〉, 〈𝑦, 𝑤〉〉(comp‘(𝐶 ×c 𝐷))〈𝑧, 𝑤〉)〈𝑓, ((Id‘𝐷)‘𝑤)〉)) = (((〈𝑦, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)‘〈𝑔, ((Id‘𝐷)‘𝑤)〉)(〈((1st ‘𝐹)‘〈𝑥, 𝑤〉), ((1st ‘𝐹)‘〈𝑦, 𝑤〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑧, 𝑤〉))((〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑦, 𝑤〉)‘〈𝑓, ((Id‘𝐷)‘𝑤)〉))) |
| 164 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(comp‘𝐷) =
(comp‘𝐷) |
| 165 | 63, 2, 6, 9, 7, 114, 115, 120, 115, 26, 164, 147, 127, 115, 140, 156, 134, 156 | xpcco2 18232 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (〈𝑔, ((Id‘𝐷)‘𝑤)〉(〈〈𝑥, 𝑤〉, 〈𝑦, 𝑤〉〉(comp‘(𝐶 ×c 𝐷))〈𝑧, 𝑤〉)〈𝑓, ((Id‘𝐷)‘𝑤)〉) = 〈(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓), (((Id‘𝐷)‘𝑤)(〈𝑤, 𝑤〉(comp‘𝐷)𝑤)((Id‘𝐷)‘𝑤))〉) |
| 166 | 6, 7, 10, 110, 115, 164, 115, 156 | catlid 17726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (((Id‘𝐷)‘𝑤)(〈𝑤, 𝑤〉(comp‘𝐷)𝑤)((Id‘𝐷)‘𝑤)) = ((Id‘𝐷)‘𝑤)) |
| 167 | 166 | opeq2d 4880 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → 〈(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓), (((Id‘𝐷)‘𝑤)(〈𝑤, 𝑤〉(comp‘𝐷)𝑤)((Id‘𝐷)‘𝑤))〉 = 〈(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓), ((Id‘𝐷)‘𝑤)〉) |
| 168 | 165, 167 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → (〈𝑔, ((Id‘𝐷)‘𝑤)〉(〈〈𝑥, 𝑤〉, 〈𝑦, 𝑤〉〉(comp‘(𝐶 ×c 𝐷))〈𝑧, 𝑤〉)〈𝑓, ((Id‘𝐷)‘𝑤)〉) = 〈(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓), ((Id‘𝐷)‘𝑤)〉) |
| 169 | 168 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)‘(〈𝑔, ((Id‘𝐷)‘𝑤)〉(〈〈𝑥, 𝑤〉, 〈𝑦, 𝑤〉〉(comp‘(𝐶 ×c 𝐷))〈𝑧, 𝑤〉)〈𝑓, ((Id‘𝐷)‘𝑤)〉)) = ((〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)‘〈(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓), ((Id‘𝐷)‘𝑤)〉)) |
| 170 | | df-ov 7434 |
. . . . . . . 8
⊢ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)(〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)((Id‘𝐷)‘𝑤)) = ((〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)‘〈(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓), ((Id‘𝐷)‘𝑤)〉) |
| 171 | 169, 170 | eqtr4di 2795 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)‘(〈𝑔, ((Id‘𝐷)‘𝑤)〉(〈〈𝑥, 𝑤〉, 〈𝑦, 𝑤〉〉(comp‘(𝐶 ×c 𝐷))〈𝑧, 𝑤〉)〈𝑓, ((Id‘𝐷)‘𝑤)〉)) = ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)(〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)((Id‘𝐷)‘𝑤))) |
| 172 | 145, 163,
171 | 3eqtr2rd 2784 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) ∧ 𝑤 ∈ (Base‘𝐷)) → ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)(〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)((Id‘𝐷)‘𝑤)) = ((((𝑦(2nd ‘𝐺)𝑧)‘𝑔)‘𝑤)(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑤), ((1st ‘((1st
‘𝐺)‘𝑦))‘𝑤)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑧))‘𝑤))(((𝑥(2nd ‘𝐺)𝑦)‘𝑓)‘𝑤))) |
| 173 | 172 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑤 ∈ (Base‘𝐷) ↦ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)(〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)((Id‘𝐷)‘𝑤))) = (𝑤 ∈ (Base‘𝐷) ↦ ((((𝑦(2nd ‘𝐺)𝑧)‘𝑔)‘𝑤)(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑤), ((1st ‘((1st
‘𝐺)‘𝑦))‘𝑤)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑧))‘𝑤))(((𝑥(2nd ‘𝐺)𝑦)‘𝑓)‘𝑤)))) |
| 174 | 2, 9, 26, 107, 113, 119, 126, 139, 133 | catcocl 17728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
| 175 | | eqid 2737 |
. . . . . 6
⊢ ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) |
| 176 | 1, 2, 107, 109, 111, 6, 9, 10, 113, 126, 174, 175 | curf2 18274 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (𝑤 ∈ (Base‘𝐷) ↦ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)(〈𝑥, 𝑤〉(2nd ‘𝐹)〈𝑧, 𝑤〉)((Id‘𝐷)‘𝑤)))) |
| 177 | 1, 2, 107, 109, 111, 6, 9, 10, 113, 119, 139, 141, 23 | curf2cl 18276 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑓) ∈ (((1st ‘𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑦))) |
| 178 | 1, 2, 107, 109, 111, 6, 9, 10, 119, 126, 133, 135, 23 | curf2cl 18276 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐺)𝑧)‘𝑔) ∈ (((1st ‘𝐺)‘𝑦)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑧))) |
| 179 | 21, 23, 6, 148, 27, 177, 178 | fucco 18010 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)〉(comp‘𝑄)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓)) = (𝑤 ∈ (Base‘𝐷) ↦ ((((𝑦(2nd ‘𝐺)𝑧)‘𝑔)‘𝑤)(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑤), ((1st ‘((1st
‘𝐺)‘𝑦))‘𝑤)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑧))‘𝑤))(((𝑥(2nd ‘𝐺)𝑦)‘𝑓)‘𝑤)))) |
| 180 | 173, 176,
179 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)〉(comp‘𝑄)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓))) |
| 181 | 2, 22, 9, 24, 8, 25, 26, 27, 3, 31, 40, 46, 62, 106, 180 | isfuncd 17910 |
. . 3
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝑄)(2nd ‘𝐺)) |
| 182 | | df-br 5144 |
. . 3
⊢
((1st ‘𝐺)(𝐶 Func 𝑄)(2nd ‘𝐺) ↔ 〈(1st ‘𝐺), (2nd ‘𝐺)〉 ∈ (𝐶 Func 𝑄)) |
| 183 | 181, 182 | sylib 218 |
. 2
⊢ (𝜑 → 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∈
(𝐶 Func 𝑄)) |
| 184 | 20, 183 | eqeltrd 2841 |
1
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝑄)) |