| Step | Hyp | Ref
| Expression |
| 1 | | 1stfval.p |
. 2
⊢ 𝑃 = (𝐶 1stF 𝐷) |
| 2 | | 1stfval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 3 | | 1stfval.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 4 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝑐)
∈ V |
| 5 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝑑)
∈ V |
| 6 | 4, 5 | xpex 7773 |
. . . . . 6
⊢
((Base‘𝑐)
× (Base‘𝑑))
∈ V |
| 7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((Base‘𝑐) × (Base‘𝑑)) ∈ V) |
| 8 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → 𝑐 = 𝐶) |
| 9 | 8 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (Base‘𝑐) = (Base‘𝐶)) |
| 10 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
| 11 | 10 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (Base‘𝑑) = (Base‘𝐷)) |
| 12 | 9, 11 | xpeq12d 5716 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((Base‘𝑐) × (Base‘𝑑)) = ((Base‘𝐶) × (Base‘𝐷))) |
| 13 | | 1stfval.t |
. . . . . . . 8
⊢ 𝑇 = (𝐶 ×c 𝐷) |
| 14 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 15 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 16 | 13, 14, 15 | xpcbas 18223 |
. . . . . . 7
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
(Base‘𝑇) |
| 17 | | 1stfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑇) |
| 18 | 16, 17 | eqtr4i 2768 |
. . . . . 6
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
𝐵 |
| 19 | 12, 18 | eqtrdi 2793 |
. . . . 5
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((Base‘𝑐) × (Base‘𝑑)) = 𝐵) |
| 20 | | simpr 484 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
| 21 | 20 | reseq2d 5997 |
. . . . . 6
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (1st ↾ 𝑏) = (1st ↾
𝐵)) |
| 22 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶) |
| 23 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷) |
| 24 | 22, 23 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑐 ×c 𝑑) = (𝐶 ×c 𝐷)) |
| 25 | 24, 13 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑐 ×c 𝑑) = 𝑇) |
| 26 | 25 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (Hom ‘(𝑐 ×c 𝑑)) = (Hom ‘𝑇)) |
| 27 | | 1stfval.h |
. . . . . . . . . 10
⊢ 𝐻 = (Hom ‘𝑇) |
| 28 | 26, 27 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (Hom ‘(𝑐 ×c 𝑑)) = 𝐻) |
| 29 | 28 | oveqd 7448 |
. . . . . . . 8
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦) = (𝑥𝐻𝑦)) |
| 30 | 29 | reseq2d 5997 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦)) = (1st ↾ (𝑥𝐻𝑦))) |
| 31 | 20, 20, 30 | mpoeq123dv 7508 |
. . . . . 6
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))) |
| 32 | 21, 31 | opeq12d 4881 |
. . . . 5
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 〈(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦)))〉 = 〈(1st ↾
𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |
| 33 | 7, 19, 32 | csbied2 3936 |
. . . 4
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ⦋((Base‘𝑐) × (Base‘𝑑)) / 𝑏⦌〈(1st ↾
𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦)))〉 = 〈(1st ↾
𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |
| 34 | | df-1stf 18218 |
. . . 4
⊢
1stF = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦
⦋((Base‘𝑐) × (Base‘𝑑)) / 𝑏⦌〈(1st ↾
𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦)))〉) |
| 35 | | opex 5469 |
. . . 4
⊢
〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉 ∈ V |
| 36 | 33, 34, 35 | ovmpoa 7588 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶
1stF 𝐷) = 〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |
| 37 | 2, 3, 36 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐶 1stF 𝐷) = 〈(1st
↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |
| 38 | 1, 37 | eqtrid 2789 |
1
⊢ (𝜑 → 𝑃 = 〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |