Step | Hyp | Ref
| Expression |
1 | | dfss2 3557 |
. . . . . . . . 9
⊢ (𝑥 ⊆ {𝐴} ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ {𝐴})) |
2 | | velsn 4141 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝐴} ↔ 𝑦 = 𝐴) |
3 | 2 | imbi2i 325 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑥 → 𝑦 ∈ {𝐴}) ↔ (𝑦 ∈ 𝑥 → 𝑦 = 𝐴)) |
4 | 3 | albii 1737 |
. . . . . . . . 9
⊢
(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = 𝐴)) |
5 | 1, 4 | bitri 263 |
. . . . . . . 8
⊢ (𝑥 ⊆ {𝐴} ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = 𝐴)) |
6 | | neq0 3889 |
. . . . . . . . . 10
⊢ (¬
𝑥 = ∅ ↔
∃𝑦 𝑦 ∈ 𝑥) |
7 | | exintr 1810 |
. . . . . . . . . 10
⊢
(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = 𝐴) → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = 𝐴))) |
8 | 6, 7 | syl5bi 231 |
. . . . . . . . 9
⊢
(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = 𝐴) → (¬ 𝑥 = ∅ → ∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = 𝐴))) |
9 | | df-clel 2606 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑥)) |
10 | | exancom 1774 |
. . . . . . . . . . 11
⊢
(∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑥) ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = 𝐴)) |
11 | 9, 10 | bitr2i 264 |
. . . . . . . . . 10
⊢
(∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = 𝐴) ↔ 𝐴 ∈ 𝑥) |
12 | | snssi 4280 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑥 → {𝐴} ⊆ 𝑥) |
13 | 11, 12 | sylbi 206 |
. . . . . . . . 9
⊢
(∃𝑦(𝑦 ∈ 𝑥 ∧ 𝑦 = 𝐴) → {𝐴} ⊆ 𝑥) |
14 | 8, 13 | syl6 34 |
. . . . . . . 8
⊢
(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 = 𝐴) → (¬ 𝑥 = ∅ → {𝐴} ⊆ 𝑥)) |
15 | 5, 14 | sylbi 206 |
. . . . . . 7
⊢ (𝑥 ⊆ {𝐴} → (¬ 𝑥 = ∅ → {𝐴} ⊆ 𝑥)) |
16 | 15 | anc2li 578 |
. . . . . 6
⊢ (𝑥 ⊆ {𝐴} → (¬ 𝑥 = ∅ → (𝑥 ⊆ {𝐴} ∧ {𝐴} ⊆ 𝑥))) |
17 | | eqss 3583 |
. . . . . 6
⊢ (𝑥 = {𝐴} ↔ (𝑥 ⊆ {𝐴} ∧ {𝐴} ⊆ 𝑥)) |
18 | 16, 17 | syl6ibr 241 |
. . . . 5
⊢ (𝑥 ⊆ {𝐴} → (¬ 𝑥 = ∅ → 𝑥 = {𝐴})) |
19 | 18 | orrd 392 |
. . . 4
⊢ (𝑥 ⊆ {𝐴} → (𝑥 = ∅ ∨ 𝑥 = {𝐴})) |
20 | | 0ss 3924 |
. . . . . 6
⊢ ∅
⊆ {𝐴} |
21 | | sseq1 3589 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ⊆ {𝐴} ↔ ∅ ⊆ {𝐴})) |
22 | 20, 21 | mpbiri 247 |
. . . . 5
⊢ (𝑥 = ∅ → 𝑥 ⊆ {𝐴}) |
23 | | eqimss 3620 |
. . . . 5
⊢ (𝑥 = {𝐴} → 𝑥 ⊆ {𝐴}) |
24 | 22, 23 | jaoi 393 |
. . . 4
⊢ ((𝑥 = ∅ ∨ 𝑥 = {𝐴}) → 𝑥 ⊆ {𝐴}) |
25 | 19, 24 | impbii 198 |
. . 3
⊢ (𝑥 ⊆ {𝐴} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐴})) |
26 | 25 | abbii 2726 |
. 2
⊢ {𝑥 ∣ 𝑥 ⊆ {𝐴}} = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 = {𝐴})} |
27 | | df-pw 4110 |
. 2
⊢ 𝒫
{𝐴} = {𝑥 ∣ 𝑥 ⊆ {𝐴}} |
28 | | dfpr2 4143 |
. 2
⊢ {∅,
{𝐴}} = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 = {𝐴})} |
29 | 26, 27, 28 | 3eqtr4i 2642 |
1
⊢ 𝒫
{𝐴} = {∅, {𝐴}} |