Metamath Proof Explorer
Description: The empty set is greater than any set of surreals. Deduction version.
(Contributed by Scott Fenton, 27-Feb-2026)
|
|
Ref |
Expression |
|
Hypotheses |
nulsltsd.1 |
|- ( ph -> A e. V ) |
|
|
nulsltsd.2 |
|- ( ph -> A C_ No ) |
|
Assertion |
nulsgtsd |
|- ( ph -> A < |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
nulsltsd.1 |
|- ( ph -> A e. V ) |
| 2 |
|
nulsltsd.2 |
|- ( ph -> A C_ No ) |
| 3 |
1 2
|
elpwd |
|- ( ph -> A e. ~P No ) |
| 4 |
|
nulsgts |
|- ( A e. ~P No -> A < |
| 5 |
3 4
|
syl |
|- ( ph -> A < |