Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nulsslt Structured version   Visualization version   GIF version

Theorem nulsslt 33370
 Description: The empty set is less than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
Assertion
Ref Expression
nulsslt (𝐴 ∈ 𝒫 No → ∅ <<s 𝐴)

Proof of Theorem nulsslt
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3462 . . 3 (𝐴 ∈ 𝒫 No 𝐴 ∈ V)
2 0ex 5178 . . 3 ∅ ∈ V
31, 2jctil 523 . 2 (𝐴 ∈ 𝒫 No → (∅ ∈ V ∧ 𝐴 ∈ V))
4 0ss 4307 . . . 4 ∅ ⊆ No
54a1i 11 . . 3 (𝐴 ∈ 𝒫 No → ∅ ⊆ No )
6 elpwi 4509 . . 3 (𝐴 ∈ 𝒫 No 𝐴 No )
7 ral0 4417 . . . 4 𝑥 ∈ ∅ ∀𝑦𝐴 𝑥 <s 𝑦
87a1i 11 . . 3 (𝐴 ∈ 𝒫 No → ∀𝑥 ∈ ∅ ∀𝑦𝐴 𝑥 <s 𝑦)
95, 6, 83jca 1125 . 2 (𝐴 ∈ 𝒫 No → (∅ ⊆ No 𝐴 No ∧ ∀𝑥 ∈ ∅ ∀𝑦𝐴 𝑥 <s 𝑦))
10 brsslt 33362 . 2 (∅ <<s 𝐴 ↔ ((∅ ∈ V ∧ 𝐴 ∈ V) ∧ (∅ ⊆ No 𝐴 No ∧ ∀𝑥 ∈ ∅ ∀𝑦𝐴 𝑥 <s 𝑦)))
113, 9, 10sylanbrc 586 1 (𝐴 ∈ 𝒫 No → ∅ <<s 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   ∈ wcel 2112  ∀wral 3109  Vcvv 3444   ⊆ wss 3884  ∅c0 4246  𝒫 cpw 4500   class class class wbr 5033   No csur 33255
 Copyright terms: Public domain W3C validator