Proof of Theorem exmidpw
Step | Hyp | Ref
| Expression |
1 | | df1o2 6326 |
. . . . 5
⊢
1o = {∅} |
2 | | p0ex 4112 |
. . . . 5
⊢ {∅}
∈ V |
3 | 1, 2 | eqeltri 2212 |
. . . 4
⊢
1o ∈ V |
4 | 3 | pwex 4107 |
. . 3
⊢ 𝒫
1o ∈ V |
5 | | exmid01 4121 |
. . . . . . . . 9
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
6 | 5 | biimpi 119 |
. . . . . . . 8
⊢
(EXMID → ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
7 | 6 | 19.21bi 1537 |
. . . . . . 7
⊢
(EXMID → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
8 | 1 | pweqi 3514 |
. . . . . . . . 9
⊢ 𝒫
1o = 𝒫 {∅} |
9 | 8 | eleq2i 2206 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 1o
↔ 𝑥 ∈ 𝒫
{∅}) |
10 | | velpw 3517 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 {∅}
↔ 𝑥 ⊆
{∅}) |
11 | 9, 10 | bitri 183 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 1o
↔ 𝑥 ⊆
{∅}) |
12 | | vex 2689 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
13 | 12 | elpr 3548 |
. . . . . . 7
⊢ (𝑥 ∈ {∅, {∅}}
↔ (𝑥 = ∅ ∨
𝑥 =
{∅})) |
14 | 7, 11, 13 | 3imtr4g 204 |
. . . . . 6
⊢
(EXMID → (𝑥 ∈ 𝒫 1o → 𝑥 ∈ {∅,
{∅}})) |
15 | 14 | ssrdv 3103 |
. . . . 5
⊢
(EXMID → 𝒫 1o ⊆ {∅,
{∅}}) |
16 | | pwpw0ss 3731 |
. . . . . . 7
⊢ {∅,
{∅}} ⊆ 𝒫 {∅} |
17 | 16, 8 | sseqtrri 3132 |
. . . . . 6
⊢ {∅,
{∅}} ⊆ 𝒫 1o |
18 | 17 | a1i 9 |
. . . . 5
⊢
(EXMID → {∅, {∅}} ⊆ 𝒫
1o) |
19 | 15, 18 | eqssd 3114 |
. . . 4
⊢
(EXMID → 𝒫 1o = {∅,
{∅}}) |
20 | | df2o2 6328 |
. . . 4
⊢
2o = {∅, {∅}} |
21 | 19, 20 | syl6eqr 2190 |
. . 3
⊢
(EXMID → 𝒫 1o =
2o) |
22 | | eqeng 6660 |
. . 3
⊢
(𝒫 1o ∈ V → (𝒫 1o =
2o → 𝒫 1o ≈
2o)) |
23 | 4, 21, 22 | mpsyl 65 |
. 2
⊢
(EXMID → 𝒫 1o ≈
2o) |
24 | | 0nep0 4089 |
. . . . . . . 8
⊢ ∅
≠ {∅} |
25 | | 0ex 4055 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
26 | 25, 2 | prss 3676 |
. . . . . . . . . 10
⊢ ((∅
∈ 𝒫 1o ∧ {∅} ∈ 𝒫 1o)
↔ {∅, {∅}} ⊆ 𝒫 1o) |
27 | 17, 26 | mpbir 145 |
. . . . . . . . 9
⊢ (∅
∈ 𝒫 1o ∧ {∅} ∈ 𝒫
1o) |
28 | | en2eqpr 6801 |
. . . . . . . . . 10
⊢
((𝒫 1o ≈ 2o ∧ ∅ ∈
𝒫 1o ∧ {∅} ∈ 𝒫 1o) →
(∅ ≠ {∅} → 𝒫 1o = {∅,
{∅}})) |
29 | 28 | 3expb 1182 |
. . . . . . . . 9
⊢
((𝒫 1o ≈ 2o ∧ (∅ ∈
𝒫 1o ∧ {∅} ∈ 𝒫 1o)) →
(∅ ≠ {∅} → 𝒫 1o = {∅,
{∅}})) |
30 | 27, 29 | mpan2 421 |
. . . . . . . 8
⊢
(𝒫 1o ≈ 2o → (∅ ≠
{∅} → 𝒫 1o = {∅,
{∅}})) |
31 | 24, 30 | mpi 15 |
. . . . . . 7
⊢
(𝒫 1o ≈ 2o → 𝒫
1o = {∅, {∅}}) |
32 | 31 | eleq2d 2209 |
. . . . . 6
⊢
(𝒫 1o ≈ 2o → (𝑥 ∈ 𝒫 1o
↔ 𝑥 ∈ {∅,
{∅}})) |
33 | 32, 11, 13 | 3bitr3g 221 |
. . . . 5
⊢
(𝒫 1o ≈ 2o → (𝑥 ⊆ {∅} ↔ (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
34 | 33 | biimpd 143 |
. . . 4
⊢
(𝒫 1o ≈ 2o → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
35 | 34 | alrimiv 1846 |
. . 3
⊢
(𝒫 1o ≈ 2o → ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
36 | 35, 5 | sylibr 133 |
. 2
⊢
(𝒫 1o ≈ 2o →
EXMID) |
37 | 23, 36 | impbii 125 |
1
⊢
(EXMID ↔ 𝒫 1o ≈
2o) |