Metamath Proof Explorer


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 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }