Step | Hyp | Ref
| Expression |
1 | | 1stfval.p |
. 2
⊢ 𝑃 = (𝐶 1stF 𝐷) |
2 | | 1stfval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | 1stfval.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ Cat) |
4 | | fvex 6784 |
. . . . . . 7
⊢
(Base‘𝑐)
∈ V |
5 | | fvex 6784 |
. . . . . . 7
⊢
(Base‘𝑑)
∈ V |
6 | 4, 5 | xpex 7597 |
. . . . . 6
⊢
((Base‘𝑐)
× (Base‘𝑑))
∈ V |
7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((Base‘𝑐) × (Base‘𝑑)) ∈ V) |
8 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → 𝑐 = 𝐶) |
9 | 8 | fveq2d 6775 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (Base‘𝑐) = (Base‘𝐶)) |
10 | | simpr 485 |
. . . . . . . 8
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
11 | 10 | fveq2d 6775 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (Base‘𝑑) = (Base‘𝐷)) |
12 | 9, 11 | xpeq12d 5621 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((Base‘𝑐) × (Base‘𝑑)) = ((Base‘𝐶) × (Base‘𝐷))) |
13 | | 1stfval.t |
. . . . . . . 8
⊢ 𝑇 = (𝐶 ×c 𝐷) |
14 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) |
15 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
16 | 13, 14, 15 | xpcbas 17893 |
. . . . . . 7
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
(Base‘𝑇) |
17 | | 1stfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑇) |
18 | 16, 17 | eqtr4i 2771 |
. . . . . 6
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
𝐵 |
19 | 12, 18 | eqtrdi 2796 |
. . . . 5
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((Base‘𝑐) × (Base‘𝑑)) = 𝐵) |
20 | | simpr 485 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
21 | 20 | reseq2d 5890 |
. . . . . 6
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (1st ↾ 𝑏) = (1st ↾
𝐵)) |
22 | | simpll 764 |
. . . . . . . . . . . . 13
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶) |
23 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷) |
24 | 22, 23 | oveq12d 7289 |
. . . . . . . . . . . 12
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑐 ×c 𝑑) = (𝐶 ×c 𝐷)) |
25 | 24, 13 | eqtr4di 2798 |
. . . . . . . . . . 11
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑐 ×c 𝑑) = 𝑇) |
26 | 25 | fveq2d 6775 |
. . . . . . . . . 10
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (Hom ‘(𝑐 ×c 𝑑)) = (Hom ‘𝑇)) |
27 | | 1stfval.h |
. . . . . . . . . 10
⊢ 𝐻 = (Hom ‘𝑇) |
28 | 26, 27 | eqtr4di 2798 |
. . . . . . . . 9
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (Hom ‘(𝑐 ×c 𝑑)) = 𝐻) |
29 | 28 | oveqd 7288 |
. . . . . . . 8
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦) = (𝑥𝐻𝑦)) |
30 | 29 | reseq2d 5890 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦)) = (1st ↾ (𝑥𝐻𝑦))) |
31 | 20, 20, 30 | mpoeq123dv 7344 |
. . . . . 6
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))) |
32 | 21, 31 | opeq12d 4818 |
. . . . 5
⊢ (((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 〈(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦)))〉 = 〈(1st ↾
𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |
33 | 7, 19, 32 | csbied2 3877 |
. . . 4
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ⦋((Base‘𝑐) × (Base‘𝑑)) / 𝑏⦌〈(1st ↾
𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦)))〉 = 〈(1st ↾
𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |
34 | | df-1stf 17888 |
. . . 4
⊢
1stF = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦
⦋((Base‘𝑐) × (Base‘𝑑)) / 𝑏⦌〈(1st ↾
𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑐 ×c 𝑑))𝑦)))〉) |
35 | | opex 5383 |
. . . 4
⊢
〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉 ∈ V |
36 | 33, 34, 35 | ovmpoa 7422 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶
1stF 𝐷) = 〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |
37 | 2, 3, 36 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐶 1stF 𝐷) = 〈(1st
↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |
38 | 1, 37 | eqtrid 2792 |
1
⊢ (𝜑 → 𝑃 = 〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) |