Proof of Theorem exmidpw
Step | Hyp | Ref
| Expression |
1 | | df1o2 6126 |
. . . . 5
⊢
1𝑜 = {∅} |
2 | | p0ex 3987 |
. . . . 5
⊢ {∅}
∈ V |
3 | 1, 2 | eqeltri 2155 |
. . . 4
⊢
1𝑜 ∈ V |
4 | 3 | pwex 3982 |
. . 3
⊢ 𝒫
1𝑜 ∈ V |
5 | | exmid01 3996 |
. . . . . . . . 9
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
6 | 5 | biimpi 118 |
. . . . . . . 8
⊢
(EXMID → ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
7 | 6 | 19.21bi 1491 |
. . . . . . 7
⊢
(EXMID → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
8 | 1 | pweqi 3410 |
. . . . . . . . 9
⊢ 𝒫
1𝑜 = 𝒫 {∅} |
9 | 8 | eleq2i 2149 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫
1𝑜 ↔ 𝑥 ∈ 𝒫 {∅}) |
10 | | selpw 3413 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 {∅}
↔ 𝑥 ⊆
{∅}) |
11 | 9, 10 | bitri 182 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫
1𝑜 ↔ 𝑥 ⊆ {∅}) |
12 | | vex 2615 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
13 | 12 | elpr 3443 |
. . . . . . 7
⊢ (𝑥 ∈ {∅, {∅}}
↔ (𝑥 = ∅ ∨
𝑥 =
{∅})) |
14 | 7, 11, 13 | 3imtr4g 203 |
. . . . . 6
⊢
(EXMID → (𝑥 ∈ 𝒫 1𝑜
→ 𝑥 ∈ {∅,
{∅}})) |
15 | 14 | ssrdv 3016 |
. . . . 5
⊢
(EXMID → 𝒫 1𝑜 ⊆
{∅, {∅}}) |
16 | | pwpw0ss 3622 |
. . . . . . 7
⊢ {∅,
{∅}} ⊆ 𝒫 {∅} |
17 | 16, 8 | sseqtr4i 3043 |
. . . . . 6
⊢ {∅,
{∅}} ⊆ 𝒫 1𝑜 |
18 | 17 | a1i 9 |
. . . . 5
⊢
(EXMID → {∅, {∅}} ⊆ 𝒫
1𝑜) |
19 | 15, 18 | eqssd 3027 |
. . . 4
⊢
(EXMID → 𝒫 1𝑜 = {∅,
{∅}}) |
20 | | df2o2 6128 |
. . . 4
⊢
2𝑜 = {∅, {∅}} |
21 | 19, 20 | syl6eqr 2133 |
. . 3
⊢
(EXMID → 𝒫 1𝑜 =
2𝑜) |
22 | | eqeng 6413 |
. . 3
⊢
(𝒫 1𝑜 ∈ V → (𝒫
1𝑜 = 2𝑜 → 𝒫
1𝑜 ≈ 2𝑜)) |
23 | 4, 21, 22 | mpsyl 64 |
. 2
⊢
(EXMID → 𝒫 1𝑜 ≈
2𝑜) |
24 | | 0nep0 3965 |
. . . . . . . 8
⊢ ∅
≠ {∅} |
25 | | 0ex 3931 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
26 | 25, 2 | prss 3567 |
. . . . . . . . . 10
⊢ ((∅
∈ 𝒫 1𝑜 ∧ {∅} ∈ 𝒫
1𝑜) ↔ {∅, {∅}} ⊆ 𝒫
1𝑜) |
27 | 17, 26 | mpbir 144 |
. . . . . . . . 9
⊢ (∅
∈ 𝒫 1𝑜 ∧ {∅} ∈ 𝒫
1𝑜) |
28 | | en2eqpr 6550 |
. . . . . . . . . 10
⊢
((𝒫 1𝑜 ≈ 2𝑜 ∧
∅ ∈ 𝒫 1𝑜 ∧ {∅} ∈ 𝒫
1𝑜) → (∅ ≠ {∅} → 𝒫
1𝑜 = {∅, {∅}})) |
29 | 28 | 3expb 1140 |
. . . . . . . . 9
⊢
((𝒫 1𝑜 ≈ 2𝑜 ∧
(∅ ∈ 𝒫 1𝑜 ∧ {∅} ∈
𝒫 1𝑜)) → (∅ ≠ {∅} →
𝒫 1𝑜 = {∅, {∅}})) |
30 | 27, 29 | mpan2 416 |
. . . . . . . 8
⊢
(𝒫 1𝑜 ≈ 2𝑜 →
(∅ ≠ {∅} → 𝒫 1𝑜 = {∅,
{∅}})) |
31 | 24, 30 | mpi 15 |
. . . . . . 7
⊢
(𝒫 1𝑜 ≈ 2𝑜 →
𝒫 1𝑜 = {∅, {∅}}) |
32 | 31 | eleq2d 2152 |
. . . . . 6
⊢
(𝒫 1𝑜 ≈ 2𝑜 →
(𝑥 ∈ 𝒫
1𝑜 ↔ 𝑥 ∈ {∅,
{∅}})) |
33 | 32, 11, 13 | 3bitr3g 220 |
. . . . 5
⊢
(𝒫 1𝑜 ≈ 2𝑜 →
(𝑥 ⊆ {∅} ↔
(𝑥 = ∅ ∨ 𝑥 = {∅}))) |
34 | 33 | biimpd 142 |
. . . 4
⊢
(𝒫 1𝑜 ≈ 2𝑜 →
(𝑥 ⊆ {∅} →
(𝑥 = ∅ ∨ 𝑥 = {∅}))) |
35 | 34 | alrimiv 1797 |
. . 3
⊢
(𝒫 1𝑜 ≈ 2𝑜 →
∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
36 | 35, 5 | sylibr 132 |
. 2
⊢
(𝒫 1𝑜 ≈ 2𝑜 →
EXMID) |
37 | 23, 36 | impbii 124 |
1
⊢
(EXMID ↔ 𝒫 1𝑜 ≈
2𝑜) |