Theorem nulsgts 28192

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 5264	. . 3 ⊢ ∅ ∈ V
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ∈ V)
4		elpwi 4567	. 2 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 ⊆ No)
5		0ss 4353	. . 3 ⊢ ∅ ⊆ No
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ⊆ No)
7		noel 4286	. . . 4 ⊢ ¬ 𝑦 ∈ ∅
8	7	pm2.21i 120	. . 3 ⊢ (𝑦 ∈ ∅ → 𝑥 <s 𝑦)
9	8	3ad2ant3 1153	. 2 ⊢ ((𝐴 ∈ 𝒫 No ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅) → 𝑥 <s 𝑦)
10	1, 3, 4, 6, 9	sltsd 28184	1 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900  ∅c0 4281  𝒫 cpw 4560   class class class wbr 5106  Nocsur 28027   <s clts 28028   <<s cslts 28173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-slts 28174

This theorem is used by:  nulsgtsd  28194  0no  28225  1no  28226  bday0  28227  0lt1s  28228  bday0b  28229  bday1  28230  cutneg  28232  rightge0  28237  lltr  28278  made0  28279  elons2  28674  oncutlt  28680  oniso  28687  bdayons  28692  onaddscl  28693  onmulscl  28694  onsbnd  28697  n0cut  28750  n0bday  28768  n0fincut  28771  bdayn0p1  28785  zcuts  28823  twocut  28839  addhalfcut  28875