Step | Hyp | Ref
| Expression |
1 | | mppsval.j |
. 2
⊢ 𝐽 = (mPPSt‘𝑇) |
2 | | fveq2 6766 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (mPreSt‘𝑡) = (mPreSt‘𝑇)) |
3 | | mppsval.p |
. . . . . . . 8
⊢ 𝑃 = (mPreSt‘𝑇) |
4 | 2, 3 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (mPreSt‘𝑡) = 𝑃) |
5 | 4 | eleq2d 2824 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ↔ 〈𝑑, ℎ, 𝑎〉 ∈ 𝑃)) |
6 | | fveq2 6766 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (mCls‘𝑡) = (mCls‘𝑇)) |
7 | | mppsval.c |
. . . . . . . . 9
⊢ 𝐶 = (mCls‘𝑇) |
8 | 6, 7 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (mCls‘𝑡) = 𝐶) |
9 | 8 | oveqd 7284 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (𝑑(mCls‘𝑡)ℎ) = (𝑑𝐶ℎ)) |
10 | 9 | eleq2d 2824 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (𝑎 ∈ (𝑑(mCls‘𝑡)ℎ) ↔ 𝑎 ∈ (𝑑𝐶ℎ))) |
11 | 5, 10 | anbi12d 631 |
. . . . 5
⊢ (𝑡 = 𝑇 → ((〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ)) ↔ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))) |
12 | 11 | oprabbidv 7331 |
. . . 4
⊢ (𝑡 = 𝑇 → {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))} = {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))}) |
13 | | df-mpps 33468 |
. . . 4
⊢ mPPSt =
(𝑡 ∈ V ↦
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}) |
14 | 3 | fvexi 6780 |
. . . . 5
⊢ 𝑃 ∈ V |
15 | 3, 1, 7 | mppspstlem 33541 |
. . . . 5
⊢
{〈〈𝑑,
ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ⊆ 𝑃 |
16 | 14, 15 | ssexi 5244 |
. . . 4
⊢
{〈〈𝑑,
ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ∈ V |
17 | 12, 13, 16 | fvmpt 6867 |
. . 3
⊢ (𝑇 ∈ V →
(mPPSt‘𝑇) =
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))}) |
18 | | fvprc 6758 |
. . . 4
⊢ (¬
𝑇 ∈ V →
(mPPSt‘𝑇) =
∅) |
19 | | df-oprab 7271 |
. . . . 5
⊢
{〈〈𝑑,
ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} = {𝑥 ∣ ∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))} |
20 | | abn0 4314 |
. . . . . . 7
⊢ ({𝑥 ∣ ∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))} ≠ ∅ ↔ ∃𝑥∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))) |
21 | | elfvex 6799 |
. . . . . . . . . . 11
⊢
(〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑇) → 𝑇 ∈ V) |
22 | 21, 3 | eleq2s 2857 |
. . . . . . . . . 10
⊢
(〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 → 𝑇 ∈ V) |
23 | 22 | ad2antrl 725 |
. . . . . . . . 9
⊢ ((𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))) → 𝑇 ∈ V) |
24 | 23 | exlimivv 1935 |
. . . . . . . 8
⊢
(∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))) → 𝑇 ∈ V) |
25 | 24 | exlimivv 1935 |
. . . . . . 7
⊢
(∃𝑥∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))) → 𝑇 ∈ V) |
26 | 20, 25 | sylbi 216 |
. . . . . 6
⊢ ({𝑥 ∣ ∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))} ≠ ∅ → 𝑇 ∈ V) |
27 | 26 | necon1bi 2972 |
. . . . 5
⊢ (¬
𝑇 ∈ V → {𝑥 ∣ ∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))} = ∅) |
28 | 19, 27 | eqtrid 2790 |
. . . 4
⊢ (¬
𝑇 ∈ V →
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} = ∅) |
29 | 18, 28 | eqtr4d 2781 |
. . 3
⊢ (¬
𝑇 ∈ V →
(mPPSt‘𝑇) =
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))}) |
30 | 17, 29 | pm2.61i 182 |
. 2
⊢
(mPPSt‘𝑇) =
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} |
31 | 1, 30 | eqtri 2766 |
1
⊢ 𝐽 = {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} |