Theorem nulsgts 28167

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

Assertion

Ref	Expression
nulsgts	⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)

Proof of Theorem nulsgts

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 ∈ 𝒫 No)
2		0ex 5260	. . 3 ⊢ ∅ ∈ V
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ∈ V)
4		elpwi 4563	. 2 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 ⊆ No)
5		0ss 4349	. . 3 ⊢ ∅ ⊆ No
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ⊆ No)
7		noel 4283	. . . 4 ⊢ ¬ 𝑦 ∈ ∅
8	7	pm2.21i 120	. . 3 ⊢ (𝑦 ∈ ∅ → 𝑥 <s 𝑦)
9	8	3ad2ant3 1153	. 2 ⊢ ((𝐴 ∈ 𝒫 No ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅) → 𝑥 <s 𝑦)
10	1, 3, 4, 6, 9	sltsd 28159	1 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  ∅c0 4278  𝒫 cpw 4556   class class class wbr 5102  Nocsur 28002   <s clts 28003   <<s cslts 28148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-slts 28149

This theorem is used by:  nulsgtsd  28169  0no  28200  1no  28201  bday0  28202  0lt1s  28203  bday0b  28204  bday1  28205  cutneg  28207  rightge0  28212  lltr  28253  made0  28254  elons2  28649  oncutlt  28655  oniso  28662  bdayons  28667  onaddscl  28668  onmulscl  28669  onsbnd  28672  n0cut  28725  n0bday  28743  n0fincut  28746  bdayn0p1  28760  zcuts  28798  twocut  28814  addhalfcut  28850