Description: The empty set is less than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | nulsslt |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ex | ||
2 | 1 | a1i | |
3 | id | ||
4 | 0ss | ||
5 | 4 | a1i | |
6 | elpwi | ||
7 | noel | ||
8 | 7 | pm2.21i | |
9 | 8 | 3ad2ant2 | |
10 | 2 3 5 6 9 | ssltd |