Metamath Proof Explorer

Theorem madessno

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

Ref Expression
Assertion madessno 
|- ( _M ` A ) C_ No

Proof

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