Theorem pwsnOLD

Description: Obsolete version of pwsn as of 14-Apr-2024. Note that the proof is essentially the same once one inlines sssn in the proof of pwsn . (Contributed by NM, 5-Jun-2006) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	pwsnOLD	⊢ 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }

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		dfclel	⊢ ( 𝐴 ∈ 𝑥 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
10		exancom	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 𝑦 = 𝐴 ) )
11	9 10	bitr2i	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 𝑦 = 𝐴 ) ↔ 𝐴 ∈ 𝑥 )
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	⊢ 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }