Theorem nulsgts 27772

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 22	. 2 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 ∈ 𝒫 No )
2		0ex 5252	. . 3 ⊢ ∅ ∈ V
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ∈ V)
4		elpwi 4561	. 2 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 ⊆ No )
5		0ss 4352	. . 3 ⊢ ∅ ⊆ No
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ⊆ No )
7		noel 4290	. . . 4 ⊢ ¬ 𝑦 ∈ ∅
8	7	pm2.21i 119	. . 3 ⊢ (𝑦 ∈ ∅ → 𝑥 <s 𝑦)
9	8	3ad2ant3 1135	. 2 ⊢ ((𝐴 ∈ 𝒫 No ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅) → 𝑥 <s 𝑦)
10	1, 3, 4, 6, 9	sltsd 27764	1 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901  ∅c0 4285  𝒫 cpw 4554   class class class wbr 5098   No csur 27607   <s clts 27608   <<s cslts 27753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-slts 27754

This theorem is referenced by:  nulsgtsd  27774  0no  27805  1no  27806  bday0  27807  0lt1s  27808  bday0b  27809  bday1  27810  cutneg  27812  rightge0  27817  lltr  27858  made0  27859  elons2  28254  oncutlt  28260  oniso  28267  bdayons  28272  onaddscl  28273  onmulscl  28274  onsbnd  28277  n0cut  28330  n0bday  28348  n0fincut  28351  bdayn0p1  28365  zcuts  28403  twocut  28419  addhalfcut  28455