Theorem nulssgt 27858

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 5313	. . 3 ⊢ ∅ ∈ V
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ∈ V)
4		elpwi 4612	. 2 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 ⊆ No )
5		0ss 4406	. . 3 ⊢ ∅ ⊆ No
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ⊆ No )
7		noel 4344	. . . 4 ⊢ ¬ 𝑦 ∈ ∅
8	7	pm2.21i 119	. . 3 ⊢ (𝑦 ∈ ∅ → 𝑥 <s 𝑦)
9	8	3ad2ant3 1134	. 2 ⊢ ((𝐴 ∈ 𝒫 No ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅) → 𝑥 <s 𝑦)
10	1, 3, 4, 6, 9	ssltd 27851	1 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3478   ⊆ wss 3963  ∅c0 4339  𝒫 cpw 4605   class class class wbr 5148   No csur 27699   <s cslt 27700   <<s csslt 27840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-sslt 27841

This theorem is referenced by:  0sno  27886  1sno  27887  bday0s  27888  0slt1s  27889  bday0b  27890  bday1s  27891  lltropt  27926  made0  27927  elons2  28296  onaddscl  28301  onmulscl  28302  n0scut  28353  n0sbday  28369  zscut  28408  1p1e2s  28415  nohalf  28422  addhalfcut  28434