Theorem 0sno 27795

Description: Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)

Assertion

Ref	Expression
0sno	⊢ 0s ∈ No

Proof of Theorem 0sno

Step	Hyp	Ref	Expression
1		df-0s 27793	. 2 ⊢ 0s = (∅ |s ∅)
2		0elpw 5331	. . . 4 ⊢ ∅ ∈ 𝒫 No
3		nulssgt 27767	. . . 4 ⊢ (∅ ∈ 𝒫 No → ∅ <<s ∅)
4	2, 3	ax-mp 5	. . 3 ⊢ ∅ <<s ∅
5		scutcl 27771	. . 3 ⊢ (∅ <<s ∅ → (∅ |s ∅) ∈ No )
6	4, 5	ax-mp 5	. 2 ⊢ (∅ |s ∅) ∈ No
7	1, 6	eqeltri 2831	1 ⊢ 0s ∈ No

Syntax hints:   ∈ wcel 2109  ∅c0 4313  𝒫 cpw 4580   class class class wbr 5124  (class class class)co 7410   No csur 27608   <<s csslt 27749   |s cscut 27751   0_s c0s 27791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4889  df-int 4928  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6360  df-on 6361  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1o 8485  df-2o 8486  df-no 27611  df-slt 27612  df-bday 27613  df-sslt 27750  df-scut 27752  df-0s 27793

This theorem is referenced by:  1sno  27796  0slt1s  27798  bday1s  27800  cuteq0  27801  cutneg  27802  cuteq1  27803  sgt0ne0  27804  made0  27842  right1s  27864  0elold  27878  addsrid  27928  addslid  27932  addsproplem2  27934  addsfo  27947  sltaddpos1d  27975  sltaddpos2d  27976  addsgt0d  27978  sltp1d  27979  negs0s  27989  negs1s  27990  negsproplem2  27992  negsproplem6  27996  negscl  27999  negsid  28004  negsdi  28013  slt0neg2d  28014  subsfo  28026  negsval2  28027  subsid1  28029  posdifsd  28058  sltsubposd  28059  subsge0d  28060  muls01  28072  mulsrid  28073  mulsproplem2  28077  mulsproplem3  28078  mulsproplem4  28079  mulsproplem5  28080  mulsproplem6  28081  mulsproplem7  28082  mulsproplem8  28083  mulscl  28094  sltmul  28096  slemuld  28098  muls02  28101  mulsgt0  28104  mulsge0d  28106  sltmulneg1d  28136  mulscan2d  28139  slemul1ad  28142  sltmul12ad  28143  muls0ord  28145  precsexlem8  28173  precsexlem9  28174  precsexlem11  28176  recsex  28178  abs0s  28201  abssnid  28202  absmuls  28203  abssge0  28204  abssneg  28206  sleabs  28207  0ons  28214  peano5n0s  28269  n0ssno  28270  0n0s  28279  peano2n0s  28280  dfn0s2  28281  n0sind  28282  n0scut  28283  n0sge0  28287  nnsgt0  28288  elnns2  28290  nnsge1  28292  nnsrecgt0d  28300  seqn0sfn  28307  n0subs  28310  eucliddivs  28322  elzs2  28344  elnnzs  28346  elznns  28347  1p1e2s  28359  twocut  28366  nohalf  28367  pw2recs  28380  pw2gt0divsd  28385  pw2ge0divsd  28386  pw2divsnegd  28389  halfcut  28390  recut  28404  0reno  28405