Proof of Theorem exmidpweq
Step | Hyp | Ref
| Expression |
1 | | exmid01 4184 |
. . . . . . . 8
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
2 | 1 | biimpi 119 |
. . . . . . 7
⊢
(EXMID → ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
3 | 2 | 19.21bi 1551 |
. . . . . 6
⊢
(EXMID → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
4 | | df1o2 6408 |
. . . . . . . . 9
⊢
1o = {∅} |
5 | 4 | pweqi 3570 |
. . . . . . . 8
⊢ 𝒫
1o = 𝒫 {∅} |
6 | 5 | eleq2i 2237 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 1o
↔ 𝑥 ∈ 𝒫
{∅}) |
7 | | velpw 3573 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 {∅}
↔ 𝑥 ⊆
{∅}) |
8 | 6, 7 | bitri 183 |
. . . . . 6
⊢ (𝑥 ∈ 𝒫 1o
↔ 𝑥 ⊆
{∅}) |
9 | | vex 2733 |
. . . . . . 7
⊢ 𝑥 ∈ V |
10 | 9 | elpr 3604 |
. . . . . 6
⊢ (𝑥 ∈ {∅, {∅}}
↔ (𝑥 = ∅ ∨
𝑥 =
{∅})) |
11 | 3, 8, 10 | 3imtr4g 204 |
. . . . 5
⊢
(EXMID → (𝑥 ∈ 𝒫 1o → 𝑥 ∈ {∅,
{∅}})) |
12 | 11 | ssrdv 3153 |
. . . 4
⊢
(EXMID → 𝒫 1o ⊆ {∅,
{∅}}) |
13 | | pwpw0ss 3791 |
. . . . . 6
⊢ {∅,
{∅}} ⊆ 𝒫 {∅} |
14 | 13, 5 | sseqtrri 3182 |
. . . . 5
⊢ {∅,
{∅}} ⊆ 𝒫 1o |
15 | 14 | a1i 9 |
. . . 4
⊢
(EXMID → {∅, {∅}} ⊆ 𝒫
1o) |
16 | 12, 15 | eqssd 3164 |
. . 3
⊢
(EXMID → 𝒫 1o = {∅,
{∅}}) |
17 | | df2o2 6410 |
. . 3
⊢
2o = {∅, {∅}} |
18 | 16, 17 | eqtr4di 2221 |
. 2
⊢
(EXMID → 𝒫 1o =
2o) |
19 | | simpr 109 |
. . . . . . . . 9
⊢
((𝒫 1o = 2o ∧ 𝑥 ⊆ {∅}) → 𝑥 ⊆ {∅}) |
20 | 19, 7 | sylibr 133 |
. . . . . . . 8
⊢
((𝒫 1o = 2o ∧ 𝑥 ⊆ {∅}) → 𝑥 ∈ 𝒫 {∅}) |
21 | 20, 5 | eleqtrrdi 2264 |
. . . . . . 7
⊢
((𝒫 1o = 2o ∧ 𝑥 ⊆ {∅}) → 𝑥 ∈ 𝒫
1o) |
22 | | simpl 108 |
. . . . . . . 8
⊢
((𝒫 1o = 2o ∧ 𝑥 ⊆ {∅}) → 𝒫
1o = 2o) |
23 | 22, 17 | eqtrdi 2219 |
. . . . . . 7
⊢
((𝒫 1o = 2o ∧ 𝑥 ⊆ {∅}) → 𝒫
1o = {∅, {∅}}) |
24 | 21, 23 | eleqtrd 2249 |
. . . . . 6
⊢
((𝒫 1o = 2o ∧ 𝑥 ⊆ {∅}) → 𝑥 ∈ {∅,
{∅}}) |
25 | 24, 10 | sylib 121 |
. . . . 5
⊢
((𝒫 1o = 2o ∧ 𝑥 ⊆ {∅}) → (𝑥 = ∅ ∨ 𝑥 = {∅})) |
26 | 25 | ex 114 |
. . . 4
⊢
(𝒫 1o = 2o → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
27 | 26 | alrimiv 1867 |
. . 3
⊢
(𝒫 1o = 2o → ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
28 | 27, 1 | sylibr 133 |
. 2
⊢
(𝒫 1o = 2o →
EXMID) |
29 | 18, 28 | impbii 125 |
1
⊢
(EXMID ↔ 𝒫 1o =
2o) |