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 
|- ~P { A } = { (/) , { A } }

Proof

Step Hyp Ref Expression
1 dfss2 
 |-  ( x C_ { A } <-> A. y ( y e. x -> y e. { A } ) )
2 velsn 
 |-  ( y e. { A } <-> y = A )
3 2 imbi2i 
 |-  ( ( y e. x -> y e. { A } ) <-> ( y e. x -> y = A ) )
4 3 albii 
 |-  ( A. y ( y e. x -> y e. { A } ) <-> A. y ( y e. x -> y = A ) )
5 1 4 bitri 
 |-  ( x C_ { A } <-> A. y ( y e. x -> y = A ) )
6 neq0 
 |-  ( -. x = (/) <-> E. y y e. x )
7 exintr 
 |-  ( A. y ( y e. x -> y = A ) -> ( E. y y e. x -> E. y ( y e. x /\ y = A ) ) )
8 6 7 syl5bi 
 |-  ( A. y ( y e. x -> y = A ) -> ( -. x = (/) -> E. y ( y e. x /\ y = A ) ) )
9 dfclel 
 |-  ( A e. x <-> E. y ( y = A /\ y e. x ) )
10 exancom 
 |-  ( E. y ( y = A /\ y e. x ) <-> E. y ( y e. x /\ y = A ) )
11 9 10 bitr2i 
 |-  ( E. y ( y e. x /\ y = A ) <-> A e. x )
12 snssi 
 |-  ( A e. x -> { A } C_ x )
13 11 12 sylbi 
 |-  ( E. y ( y e. x /\ y = A ) -> { A } C_ x )
14 8 13 syl6 
 |-  ( A. y ( y e. x -> y = A ) -> ( -. x = (/) -> { A } C_ x ) )
15 5 14 sylbi 
 |-  ( x C_ { A } -> ( -. x = (/) -> { A } C_ x ) )
16 15 anc2li 
 |-  ( x C_ { A } -> ( -. x = (/) -> ( x C_ { A } /\ { A } C_ x ) ) )
17 eqss 
 |-  ( x = { A } <-> ( x C_ { A } /\ { A } C_ x ) )
18 16 17 syl6ibr 
 |-  ( x C_ { A } -> ( -. x = (/) -> x = { A } ) )
19 18 orrd 
 |-  ( x C_ { A } -> ( x = (/) \/ x = { A } ) )
20 0ss 
 |-  (/) C_ { A }
21 sseq1 
 |-  ( x = (/) -> ( x C_ { A } <-> (/) C_ { A } ) )
22 20 21 mpbiri 
 |-  ( x = (/) -> x C_ { A } )
23 eqimss 
 |-  ( x = { A } -> x C_ { A } )
24 22 23 jaoi 
 |-  ( ( x = (/) \/ x = { A } ) -> x C_ { A } )
25 19 24 impbii 
 |-  ( x C_ { A } <-> ( x = (/) \/ x = { A } ) )
26 25 abbii 
 |-  { x | x C_ { A } } = { x | ( x = (/) \/ x = { A } ) }
27 df-pw 
 |-  ~P { A } = { x | x C_ { A } }
28 dfpr2 
 |-  { (/) , { A } } = { x | ( x = (/) \/ x = { A } ) }
29 26 27 28 3eqtr4i 
 |-  ~P { A } = { (/) , { A } }