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