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

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

Proof of Theorem nulssgt
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3243 . . 3 (𝐴 ∈ 𝒫 No 𝐴 ∈ V)
2 0ex 4823 . . 3 ∅ ∈ V
31, 2jctir 560 . 2 (𝐴 ∈ 𝒫 No → (𝐴 ∈ V ∧ ∅ ∈ V))
4 elpwi 4201 . . 3 (𝐴 ∈ 𝒫 No 𝐴 No )
5 0ss 4005 . . . 4 ∅ ⊆ No
65a1i 11 . . 3 (𝐴 ∈ 𝒫 No → ∅ ⊆ No )
7 ral0 4109 . . . . 5 𝑦 ∈ ∅ 𝑥 <s 𝑦
87rgenw 2953 . . . 4 𝑥𝐴𝑦 ∈ ∅ 𝑥 <s 𝑦
98a1i 11 . . 3 (𝐴 ∈ 𝒫 No → ∀𝑥𝐴𝑦 ∈ ∅ 𝑥 <s 𝑦)
104, 6, 93jca 1261 . 2 (𝐴 ∈ 𝒫 No → (𝐴 No ∧ ∅ ⊆ No ∧ ∀𝑥𝐴𝑦 ∈ ∅ 𝑥 <s 𝑦))
11 brsslt 32025 . 2 (𝐴 <<s ∅ ↔ ((𝐴 ∈ V ∧ ∅ ∈ V) ∧ (𝐴 No ∧ ∅ ⊆ No ∧ ∀𝑥𝐴𝑦 ∈ ∅ 𝑥 <s 𝑦)))
123, 10, 11sylanbrc 699 1 (𝐴 ∈ 𝒫 No 𝐴 <<s ∅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   ∈ wcel 2030  ∀wral 2941  Vcvv 3231   ⊆ wss 3607  ∅c0 3948  𝒫 cpw 4191   class class class wbr 4685   No csur 31918
 Copyright terms: Public domain W3C validator