Description: The empty set is less than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nulsslt | |- ( A e. ~P No -> (/) < |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0ex | |- (/) e. _V |
|
| 2 | 1 | a1i | |- ( A e. ~P No -> (/) e. _V ) |
| 3 | id | |- ( A e. ~P No -> A e. ~P No ) |
|
| 4 | 0ss | |- (/) C_ No |
|
| 5 | 4 | a1i | |- ( A e. ~P No -> (/) C_ No ) |
| 6 | elpwi | |- ( A e. ~P No -> A C_ No ) |
|
| 7 | noel | |- -. x e. (/) |
|
| 8 | 7 | pm2.21i | |- ( x e. (/) -> x |
| 9 | 8 | 3ad2ant2 | |- ( ( A e. ~P No /\ x e. (/) /\ y e. A ) -> x |
| 10 | 2 3 5 6 9 | ssltd | |- ( A e. ~P No -> (/) < |