Theorem pwpw0

Description: Compute the power set of the power set of the empty set. (See pw0 for the power set of the empty set.) Theorem 90 of Suppes p. 48. Although this theorem is a special case of pwsn , we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994)

	Ref	Expression
Assertion	pwpw0	⊢ 𝒫 { ∅ } = { ∅ , { ∅ } }

Proof

Step	Hyp	Ref	Expression
1		dfss2	⊢ ( 𝑥 ⊆ { ∅ } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ { ∅ } ) )
2		velsn	⊢ ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ )
3	2	imbi2i	⊢ ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ { ∅ } ) ↔ ( 𝑦 ∈ 𝑥 → 𝑦 = ∅ ) )
4	3	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ { ∅ } ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 = ∅ ) )
5	1 4	bitri	⊢ ( 𝑥 ⊆ { ∅ } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 = ∅ ) )
6		neq0	⊢ ( ¬ 𝑥 = ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
7		exintr	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 = ∅ ) → ( ∃ 𝑦 𝑦 ∈ 𝑥 → ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 𝑦 = ∅ ) ) )
8	6 7	syl5bi	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 = ∅ ) → ( ¬ 𝑥 = ∅ → ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 𝑦 = ∅ ) ) )
9		exancom	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 𝑦 = ∅ ) ↔ ∃ 𝑦 ( 𝑦 = ∅ ∧ 𝑦 ∈ 𝑥 ) )
10		dfclel	⊢ ( ∅ ∈ 𝑥 ↔ ∃ 𝑦 ( 𝑦 = ∅ ∧ 𝑦 ∈ 𝑥 ) )
11	9 10	bitr4i	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 𝑦 = ∅ ) ↔ ∅ ∈ 𝑥 )
12		snssi	⊢ ( ∅ ∈ 𝑥 → { ∅ } ⊆ 𝑥 )
13	11 12	sylbi	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 𝑦 = ∅ ) → { ∅ } ⊆ 𝑥 )
14	8 13	syl6	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 = ∅ ) → ( ¬ 𝑥 = ∅ → { ∅ } ⊆ 𝑥 ) )
15	5 14	sylbi	⊢ ( 𝑥 ⊆ { ∅ } → ( ¬ 𝑥 = ∅ → { ∅ } ⊆ 𝑥 ) )
16	15	anc2li	⊢ ( 𝑥 ⊆ { ∅ } → ( ¬ 𝑥 = ∅ → ( 𝑥 ⊆ { ∅ } ∧ { ∅ } ⊆ 𝑥 ) ) )
17		eqss	⊢ ( 𝑥 = { ∅ } ↔ ( 𝑥 ⊆ { ∅ } ∧ { ∅ } ⊆ 𝑥 ) )
18	16 17	syl6ibr	⊢ ( 𝑥 ⊆ { ∅ } → ( ¬ 𝑥 = ∅ → 𝑥 = { ∅ } ) )
19	18	orrd	⊢ ( 𝑥 ⊆ { ∅ } → ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) )
20		0ss	⊢ ∅ ⊆ { ∅ }
21		sseq1	⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ { ∅ } ↔ ∅ ⊆ { ∅ } ) )
22	20 21	mpbiri	⊢ ( 𝑥 = ∅ → 𝑥 ⊆ { ∅ } )
23		eqimss	⊢ ( 𝑥 = { ∅ } → 𝑥 ⊆ { ∅ } )
24	22 23	jaoi	⊢ ( ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) → 𝑥 ⊆ { ∅ } )
25	19 24	impbii	⊢ ( 𝑥 ⊆ { ∅ } ↔ ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) )
26	25	abbii	⊢ { 𝑥 ∣ 𝑥 ⊆ { ∅ } } = { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) }
27		df-pw	⊢ 𝒫 { ∅ } = { 𝑥 ∣ 𝑥 ⊆ { ∅ } }
28		dfpr2	⊢ { ∅ , { ∅ } } = { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) }
29	26 27 28	3eqtr4i	⊢ 𝒫 { ∅ } = { ∅ , { ∅ } }