Theorem nulssgt 27686

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.

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 ∈ 𝒫 No )
2		0ex 5257	. . 3 ⊢ ∅ ∈ V
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ∈ V)
4		elpwi 4566	. 2 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 ⊆ No )
5		0ss 4359	. . 3 ⊢ ∅ ⊆ No
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ⊆ No )
7		noel 4297	. . . 4 ⊢ ¬ 𝑦 ∈ ∅
8	7	pm2.21i 119	. . 3 ⊢ (𝑦 ∈ ∅ → 𝑥 <s 𝑦)
9	8	3ad2ant3 1135	. 2 ⊢ ((𝐴 ∈ 𝒫 No ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅) → 𝑥 <s 𝑦)
10	1, 3, 4, 6, 9	ssltd 27679	1 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911  ∅c0 4292  𝒫 cpw 4559   class class class wbr 5102   No csur 27527   <s cslt 27528   <<s csslt 27668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-sslt 27669

This theorem is referenced by:  0sno  27714  1sno  27715  bday0s  27716  0slt1s  27717  bday0b  27718  bday1s  27719  cutneg  27721  lltropt  27760  made0  27761  elons2  28135  onscutlt  28141  onsiso  28145  bdayon  28149  onaddscl  28150  onmulscl  28151  n0scut  28202  n0sbday  28220  n0sfincut  28222  bdayn0p1  28234  zscut  28271  1p1e2s  28278  twocut  28285  addhalfcut  28310