Metamath Proof Explorer

Theorem oldssno

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

Ref Expression
Assertion oldssno 
|- ( _Old ` A ) C_ No

Proof

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