Metamath Proof Explorer

Theorem newssno

Description: New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024)

Ref Expression
Assertion newssno 
|- ( _New ` A ) C_ No

Proof

Step Hyp Ref Expression
1 newf 
 |-  _New : On --> ~P No
2 0elpw 
 |-  (/) e. ~P No
3 1 2 f0cli 
 |-  ( _New ` A ) e. ~P No
4 elpwi 
 |-  ( ( _New ` A ) e. ~P No -> ( _New ` A ) C_ No )
5 3 4 ax-mp 
 |-  ( _New ` A ) C_ No