Metamath Proof Explorer

Theorem npex

Description: The class of positive reals is a set. (Contributed by NM, 31-Oct-1995) (New usage is discouraged.)

Ref Expression
Assertion npex 
|- P. e. _V

Proof

Step Hyp Ref Expression
1 nqex 
 |-  Q. e. _V
2 1 pwex 
 |-  ~P Q. e. _V
3 pssss 
 |-  ( x C. Q. -> x C_ Q. )
4 3 ad2antlr 
 |-  ( ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z  z e. x ) /\ E. z e. x y  x C_ Q. )
5 4 ss2abi 
 |-  { x | ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z  z e. x ) /\ E. z e. x y
6 df-np 
 |-  P. = { x | ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z  z e. x ) /\ E. z e. x y
7 df-pw 
 |-  ~P Q. = { x | x C_ Q. }
8 5 6 7 3sstr4i 
 |-  P. C_ ~P Q.
9 2 8 ssexi 
 |-  P. e. _V