Step | Hyp | Ref
| Expression |
1 | | dfss2 3954 |
. . . . . . . . 9
⊢ (𝑥 ⊆ {∅} ↔
∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ {∅})) |
2 | | velsn 4576 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅) |
3 | 2 | imbi2i 338 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑥 → 𝑦 ∈ {∅}) ↔ (𝑦 ∈ 𝑥 → 𝑦 = ∅)) |
4 | 3 | albii 1816 |
. . . . . . . . 9
⊢
(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ {∅}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = ∅)) |
5 | 1, 4 | bitri 277 |
. . . . . . . 8
⊢ (𝑥 ⊆ {∅} ↔
∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = ∅)) |
6 | | neq0 4308 |
. . . . . . . . . 10
⊢ (¬
𝑥 = ∅ ↔
∃𝑦 𝑦 ∈ 𝑥) |
7 | | exintr 1889 |
. . . . . . . . . 10
⊢
(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = ∅) → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = ∅))) |
8 | 6, 7 | syl5bi 244 |
. . . . . . . . 9
⊢
(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = ∅) → (¬ 𝑥 = ∅ → ∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = ∅))) |
9 | | exancom 1857 |
. . . . . . . . . . 11
⊢
(∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = ∅) ↔ ∃𝑦(𝑦 = ∅ ∧ 𝑦 ∈ 𝑥)) |
10 | | dfclel 2894 |
. . . . . . . . . . 11
⊢ (∅
∈ 𝑥 ↔
∃𝑦(𝑦 = ∅ ∧ 𝑦 ∈ 𝑥)) |
11 | 9, 10 | bitr4i 280 |
. . . . . . . . . 10
⊢
(∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = ∅) ↔ ∅ ∈ 𝑥) |
12 | | snssi 4734 |
. . . . . . . . . 10
⊢ (∅
∈ 𝑥 → {∅}
⊆ 𝑥) |
13 | 11, 12 | sylbi 219 |
. . . . . . . . 9
⊢
(∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = ∅) → {∅} ⊆ 𝑥) |
14 | 8, 13 | syl6 35 |
. . . . . . . 8
⊢
(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = ∅) → (¬ 𝑥 = ∅ → {∅} ⊆ 𝑥)) |
15 | 5, 14 | sylbi 219 |
. . . . . . 7
⊢ (𝑥 ⊆ {∅} → (¬
𝑥 = ∅ →
{∅} ⊆ 𝑥)) |
16 | 15 | anc2li 558 |
. . . . . 6
⊢ (𝑥 ⊆ {∅} → (¬
𝑥 = ∅ → (𝑥 ⊆ {∅} ∧
{∅} ⊆ 𝑥))) |
17 | | eqss 3981 |
. . . . . 6
⊢ (𝑥 = {∅} ↔ (𝑥 ⊆ {∅} ∧
{∅} ⊆ 𝑥)) |
18 | 16, 17 | syl6ibr 254 |
. . . . 5
⊢ (𝑥 ⊆ {∅} → (¬
𝑥 = ∅ → 𝑥 = {∅})) |
19 | 18 | orrd 859 |
. . . 4
⊢ (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})) |
20 | | 0ss 4349 |
. . . . . 6
⊢ ∅
⊆ {∅} |
21 | | sseq1 3991 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ⊆ {∅} ↔
∅ ⊆ {∅})) |
22 | 20, 21 | mpbiri 260 |
. . . . 5
⊢ (𝑥 = ∅ → 𝑥 ⊆
{∅}) |
23 | | eqimss 4022 |
. . . . 5
⊢ (𝑥 = {∅} → 𝑥 ⊆
{∅}) |
24 | 22, 23 | jaoi 853 |
. . . 4
⊢ ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 ⊆
{∅}) |
25 | 19, 24 | impbii 211 |
. . 3
⊢ (𝑥 ⊆ {∅} ↔ (𝑥 = ∅ ∨ 𝑥 = {∅})) |
26 | 25 | abbii 2886 |
. 2
⊢ {𝑥 ∣ 𝑥 ⊆ {∅}} = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 = {∅})} |
27 | | df-pw 4540 |
. 2
⊢ 𝒫
{∅} = {𝑥 ∣
𝑥 ⊆
{∅}} |
28 | | dfpr2 4579 |
. 2
⊢ {∅,
{∅}} = {𝑥 ∣
(𝑥 = ∅ ∨ 𝑥 = {∅})} |
29 | 26, 27, 28 | 3eqtr4i 2854 |
1
⊢ 𝒫
{∅} = {∅, {∅}} |