Step | Hyp | Ref
| Expression |
1 | | mpstval.p |
. 2
⊢ 𝑃 = (mPreSt‘𝑇) |
2 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (mDV‘𝑡) = (mDV‘𝑇)) |
3 | | mpstval.v |
. . . . . . . . 9
⊢ 𝑉 = (mDV‘𝑇) |
4 | 2, 3 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (mDV‘𝑡) = 𝑉) |
5 | 4 | pweqd 4163 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → 𝒫 (mDV‘𝑡) = 𝒫 𝑉) |
6 | 5 | rabeqdv 3194 |
. . . . . 6
⊢ (𝑡 = 𝑇 → {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} = {𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑}) |
7 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (mEx‘𝑡) = (mEx‘𝑇)) |
8 | | mpstval.e |
. . . . . . . . 9
⊢ 𝐸 = (mEx‘𝑇) |
9 | 7, 8 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (mEx‘𝑡) = 𝐸) |
10 | 9 | pweqd 4163 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → 𝒫 (mEx‘𝑡) = 𝒫 𝐸) |
11 | 10 | ineq1d 3813 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (𝒫 (mEx‘𝑡) ∩ Fin) = (𝒫 𝐸 ∩ Fin)) |
12 | 6, 11 | xpeq12d 5140 |
. . . . 5
⊢ (𝑡 = 𝑇 → ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) = ({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin))) |
13 | 12, 9 | xpeq12d 5140 |
. . . 4
⊢ (𝑡 = 𝑇 → (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) ×
(mEx‘𝑡)) = (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)) |
14 | | df-mpst 31390 |
. . . 4
⊢ mPreSt =
(𝑡 ∈ V ↦
(({𝑑 ∈ 𝒫
(mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) ×
(mEx‘𝑡))) |
15 | | fvex 6201 |
. . . . . . . . 9
⊢
(mDV‘𝑇) ∈
V |
16 | 3, 15 | eqeltri 2697 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
17 | 16 | pwex 4848 |
. . . . . . 7
⊢ 𝒫
𝑉 ∈ V |
18 | 17 | rabex 4813 |
. . . . . 6
⊢ {𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} ∈ V |
19 | | fvex 6201 |
. . . . . . . . 9
⊢
(mEx‘𝑇) ∈
V |
20 | 8, 19 | eqeltri 2697 |
. . . . . . . 8
⊢ 𝐸 ∈ V |
21 | 20 | pwex 4848 |
. . . . . . 7
⊢ 𝒫
𝐸 ∈ V |
22 | 21 | inex1 4799 |
. . . . . 6
⊢
(𝒫 𝐸 ∩
Fin) ∈ V |
23 | 18, 22 | xpex 6962 |
. . . . 5
⊢ ({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) ∈ V |
24 | 23, 20 | xpex 6962 |
. . . 4
⊢ (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) ∈ V |
25 | 13, 14, 24 | fvmpt 6282 |
. . 3
⊢ (𝑇 ∈ V →
(mPreSt‘𝑇) = (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)) |
26 | | xp0 5552 |
. . . . 5
⊢ (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × ∅) =
∅ |
27 | 26 | eqcomi 2631 |
. . . 4
⊢ ∅ =
(({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) ×
∅) |
28 | | fvprc 6185 |
. . . 4
⊢ (¬
𝑇 ∈ V →
(mPreSt‘𝑇) =
∅) |
29 | | fvprc 6185 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mEx‘𝑇) =
∅) |
30 | 8, 29 | syl5eq 2668 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝐸 = ∅) |
31 | 30 | xpeq2d 5139 |
. . . 4
⊢ (¬
𝑇 ∈ V → (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) = (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) ×
∅)) |
32 | 27, 28, 31 | 3eqtr4a 2682 |
. . 3
⊢ (¬
𝑇 ∈ V →
(mPreSt‘𝑇) = (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)) |
33 | 25, 32 | pm2.61i 176 |
. 2
⊢
(mPreSt‘𝑇) =
(({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) |
34 | 1, 33 | eqtri 2644 |
1
⊢ 𝑃 = (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) |