Metamath Proof Explorer

Theorem noprc

Description: The surreal numbers are a proper class. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion noprc 
|- -. No e. _V

Proof

Step Hyp Ref Expression
1 onprc 
 |-  -. On e. _V
2 bdayfo 
 |-  bday : No -onto-> On
3 fornex 
 |-  ( No e. _V -> ( bday : No -onto-> On -> On e. _V ) )
4 2 3 mpi 
 |-  ( No e. _V -> On e. _V )
5 1 4 mto 
 |-  -. No e. _V