Step | Hyp | Ref
| Expression |
1 | | mppsval.j |
. 2
⊢ 𝐽 = (mPPSt‘𝑇) |
2 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (mPreSt‘𝑡) = (mPreSt‘𝑇)) |
3 | | mppsval.p |
. . . . . . . 8
⊢ 𝑃 = (mPreSt‘𝑇) |
4 | 2, 3 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (mPreSt‘𝑡) = 𝑃) |
5 | 4 | eleq2d 2673 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ↔ 〈𝑑, ℎ, 𝑎〉 ∈ 𝑃)) |
6 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (mCls‘𝑡) = (mCls‘𝑇)) |
7 | | mppsval.c |
. . . . . . . . 9
⊢ 𝐶 = (mCls‘𝑇) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (mCls‘𝑡) = 𝐶) |
9 | 8 | oveqd 6566 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (𝑑(mCls‘𝑡)ℎ) = (𝑑𝐶ℎ)) |
10 | 9 | eleq2d 2673 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (𝑎 ∈ (𝑑(mCls‘𝑡)ℎ) ↔ 𝑎 ∈ (𝑑𝐶ℎ))) |
11 | 5, 10 | anbi12d 743 |
. . . . 5
⊢ (𝑡 = 𝑇 → ((〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ)) ↔ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))) |
12 | 11 | oprabbidv 6607 |
. . . 4
⊢ (𝑡 = 𝑇 → {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))} = {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))}) |
13 | | df-mpps 30649 |
. . . 4
⊢ mPPSt =
(𝑡 ∈ V ↦
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}) |
14 | | fvex 6113 |
. . . . . 6
⊢
(mPreSt‘𝑇)
∈ V |
15 | 3, 14 | eqeltri 2684 |
. . . . 5
⊢ 𝑃 ∈ V |
16 | 3, 1, 7 | mppspstlem 30722 |
. . . . 5
⊢
{〈〈𝑑,
ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ⊆ 𝑃 |
17 | 15, 16 | ssexi 4731 |
. . . 4
⊢
{〈〈𝑑,
ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ∈ V |
18 | 12, 13, 17 | fvmpt 6191 |
. . 3
⊢ (𝑇 ∈ V →
(mPPSt‘𝑇) =
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))}) |
19 | | fvprc 6097 |
. . . 4
⊢ (¬
𝑇 ∈ V →
(mPPSt‘𝑇) =
∅) |
20 | | df-oprab 6553 |
. . . . 5
⊢
{〈〈𝑑,
ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} = {𝑥 ∣ ∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))} |
21 | | abn0 3908 |
. . . . . . 7
⊢ ({𝑥 ∣ ∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))} ≠ ∅ ↔ ∃𝑥∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))) |
22 | | elfvex 6131 |
. . . . . . . . . . 11
⊢
(〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑇) → 𝑇 ∈ V) |
23 | 22, 3 | eleq2s 2706 |
. . . . . . . . . 10
⊢
(〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 → 𝑇 ∈ V) |
24 | 23 | ad2antrl 760 |
. . . . . . . . 9
⊢ ((𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))) → 𝑇 ∈ V) |
25 | 24 | exlimivv 1847 |
. . . . . . . 8
⊢
(∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))) → 𝑇 ∈ V) |
26 | 25 | exlimivv 1847 |
. . . . . . 7
⊢
(∃𝑥∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))) → 𝑇 ∈ V) |
27 | 21, 26 | sylbi 206 |
. . . . . 6
⊢ ({𝑥 ∣ ∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))} ≠ ∅ → 𝑇 ∈ V) |
28 | 27 | necon1bi 2810 |
. . . . 5
⊢ (¬
𝑇 ∈ V → {𝑥 ∣ ∃𝑑∃ℎ∃𝑎(𝑥 = 〈〈𝑑, ℎ〉, 𝑎〉 ∧ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ)))} = ∅) |
29 | 20, 28 | syl5eq 2656 |
. . . 4
⊢ (¬
𝑇 ∈ V →
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} = ∅) |
30 | 19, 29 | eqtr4d 2647 |
. . 3
⊢ (¬
𝑇 ∈ V →
(mPPSt‘𝑇) =
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))}) |
31 | 18, 30 | pm2.61i 175 |
. 2
⊢
(mPPSt‘𝑇) =
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} |
32 | 1, 31 | eqtri 2632 |
1
⊢ 𝐽 = {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} |