Theorem pwsnALT 2505

Description: The power set of a singleton (direct proof).

Assertion

Ref	Expression
pwsnALT	⊢ ℘{A} = {∅, {A}}

Proof of Theorem pwsnALT

Step	Hyp	Ref	Expression
1		dfss2 2061	. . . . . . . . 9 ⊢ (x ⊆ {A} ↔ ∀y(y ∈ x → y ∈ {A}))
2		elsn 2425	. . . . . . . . . . 11 ⊢ (y ∈ {A} ↔ y = A)
3	2	imbi2i 185	. . . . . . . . . 10 ⊢ ((y ∈ x → y ∈ {A}) ↔ (y ∈ x → y = A))
4	3	albii 1001	. . . . . . . . 9 ⊢ (∀y(y ∈ x → y ∈ {A}) ↔ ∀y(y ∈ x → y = A))
5	1, 4	bitr 173	. . . . . . . 8 ⊢ (x ⊆ {A} ↔ ∀y(y ∈ x → y = A))
6		exintr 1119	. . . . . . . . . 10 ⊢ (∀y(y ∈ x → y = A) → (∃y y ∈ x → ∃y(y ∈ x ⋀ y = A)))
7		n0 2293	. . . . . . . . . 10 ⊢ (¬ x = ∅ ↔ ∃y y ∈ x)
8	6, 7	syl5ib 206	. . . . . . . . 9 ⊢ (∀y(y ∈ x → y = A) → (¬ x = ∅ → ∃y(y ∈ x ⋀ y = A)))
9		df-clel 1475	. . . . . . . . . . 11 ⊢ (A ∈ x ↔ ∃y(y = A ⋀ y ∈ x))
10		exancom 1056	. . . . . . . . . . 11 ⊢ (∃y(y = A ⋀ y ∈ x) ↔ ∃y(y ∈ x ⋀ y = A))
11	9, 10	bitr2 174	. . . . . . . . . 10 ⊢ (∃y(y ∈ x ⋀ y = A) ↔ A ∈ x)
12		snssi 2470	. . . . . . . . . 10 ⊢ (A ∈ x → {A} ⊆ x)
13	11, 12	sylbi 199	. . . . . . . . 9 ⊢ (∃y(y ∈ x ⋀ y = A) → {A} ⊆ x)
14	8, 13	syl6 22	. . . . . . . 8 ⊢ (∀y(y ∈ x → y = A) → (¬ x = ∅ → {A} ⊆ x))
15	5, 14	sylbi 199	. . . . . . 7 ⊢ (x ⊆ {A} → (¬ x = ∅ → {A} ⊆ x))
16	15	anc2li 302	. . . . . 6 ⊢ (x ⊆ {A} → (¬ x = ∅ → (x ⊆ {A} ⋀ {A} ⊆ x)))
17		eqss 2080	. . . . . 6 ⊢ (x = {A} ↔ (x ⊆ {A} ⋀ {A} ⊆ x))
18	16, 17	syl6ibr 213	. . . . 5 ⊢ (x ⊆ {A} → (¬ x = ∅ → x = {A}))
19	18	orrd 233	. . . 4 ⊢ (x ⊆ {A} → (x = ∅ ⋁ x = {A}))
20		0ss 2305	. . . . . 6 ⊢ ∅ ⊆ {A}
21		sseq1 2085	. . . . . 6 ⊢ (x = ∅ → (x ⊆ {A} ↔ ∅ ⊆ {A}))
22	20, 21	mpbiri 194	. . . . 5 ⊢ (x = ∅ → x ⊆ {A})
23		eqimss 2112	. . . . 5 ⊢ (x = {A} → x ⊆ {A})
24	22, 23	jaoi 341	. . . 4 ⊢ ((x = ∅ ⋁ x = {A}) → x ⊆ {A})
25	19, 24	impbi 157	. . 3 ⊢ (x ⊆ {A} ↔ (x = ∅ ⋁ x = {A}))
26	25	abbii 1578	. 2 ⊢ {x∣x ⊆ {A}} = {x∣(x = ∅ ⋁ x = {A})}
27		df-pw 2406	. 2 ⊢ ℘{A} = {x∣x ⊆ {A}}
28		dfpr2 2426	. 2 ⊢ {∅, {A}} = {x∣(x = ∅ ⋁ x = {A})}
29	26, 27, 28	3eqtr4 1508	1 ⊢ ℘{A} = {∅, {A}}

Syntax hints:  ¬ wn 2   → wi 3   ⋁ wo 222   ⋀ wa 223  ∀wal 956   = wceq 958   ∈ wcel 960  ∃wex 982  {cab 1466   ⊆ wss 2050  ∅c0 2283  ℘cpw 2405  {csn 2413  {cpr 2414

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417

Copyright terms: Public domain