Metamath Proof Explorer


Theorem nulsslt

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

Ref Expression
Assertion nulsslt A 𝒫 No s A

Proof

Step Hyp Ref Expression
1 0ex V
2 1 a1i A 𝒫 No V
3 id A 𝒫 No A 𝒫 No
4 0ss No
5 4 a1i A 𝒫 No No
6 elpwi A 𝒫 No A No
7 noel ¬ x
8 7 pm2.21i x x < s y
9 8 3ad2ant2 A 𝒫 No x y A x < s y
10 2 3 5 6 9 ssltd A 𝒫 No s A