Metamath Proof Explorer

Theorem nulssgt

Description: The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion nulssgt 
|- ( A e. ~P No -> A <

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. ~P No -> A e. ~P No )
2 0ex 
 |-  (/) e. _V
3 2 a1i 
 |-  ( A e. ~P No -> (/) e. _V )
4 elpwi 
 |-  ( A e. ~P No -> A C_ No )
5 0ss 
 |-  (/) C_ No
6 5 a1i 
 |-  ( A e. ~P No -> (/) C_ No )
7 noel 
 |-  -. y e. (/)
8 7 pm2.21i 
 |-  ( y e. (/) -> x
9 8 3ad2ant3 
 |-  ( ( A e. ~P No /\ x e. A /\ y e. (/) ) -> x
10 1 3 4 6 9 ssltd 
 |-  ( A e. ~P No -> A <