Theorem nulssgt 27798

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 5289	. . 3 ⊢ ∅ ∈ V
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ∈ V)
4		elpwi 4589	. 2 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 ⊆ No )
5		0ss 4382	. . 3 ⊢ ∅ ⊆ No
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝒫 No → ∅ ⊆ No )
7		noel 4320	. . . 4 ⊢ ¬ 𝑦 ∈ ∅
8	7	pm2.21i 119	. . 3 ⊢ (𝑦 ∈ ∅ → 𝑥 <s 𝑦)
9	8	3ad2ant3 1135	. 2 ⊢ ((𝐴 ∈ 𝒫 No ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅) → 𝑥 <s 𝑦)
10	1, 3, 4, 6, 9	ssltd 27791	1 ⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3464   ⊆ wss 3933  ∅c0 4315  𝒫 cpw 4582   class class class wbr 5125   No csur 27639   <s cslt 27640   <<s csslt 27780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pr 5414

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-br 5126  df-opab 5188  df-xp 5673  df-sslt 27781

This theorem is referenced by:  0sno  27826  1sno  27827  bday0s  27828  0slt1s  27829  bday0b  27830  bday1s  27831  lltropt  27866  made0  27867  elons2  28236  onaddscl  28241  onmulscl  28242  n0scut  28293  n0sbday  28309  zscut  28348  1p1e2s  28355  nohalf  28362  addhalfcut  28374