Theorem 0no 27826

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

Assertion

Ref	Expression
0no	⊢ 0s ∈ No

Proof of Theorem 0no

Step	Hyp	Ref	Expression
1		df-0s 27824	. 2 ⊢ 0s = (∅ |s ∅)
2		0elpw 5291	. . . 4 ⊢ ∅ ∈ 𝒫 No
3		nulsgts 27793	. . . 4 ⊢ (∅ ∈ 𝒫 No → ∅ <<s ∅)
4	2, 3	ax-mp 5	. . 3 ⊢ ∅ <<s ∅
5		cutscl 27799	. . 3 ⊢ (∅ <<s ∅ → (∅ |s ∅) ∈ No )
6	4, 5	ax-mp 5	. 2 ⊢ (∅ |s ∅) ∈ No
7	1, 6	eqeltri 2836	1 ⊢ 0s ∈ No

Syntax hints:   ∈ wcel 2119  ∅c0 4268  𝒫 cpw 4536   class class class wbr 5079  (class class class)co 7363   No csur 27628   <<s cslts 27774   |s ccuts 27776   0_s c0s 27822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-int 4885  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6320  df-on 6321  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1o 8402  df-2o 8403  df-no 27631  df-lts 27632  df-bday 27633  df-slts 27775  df-cuts 27777  df-0s 27824

This theorem is referenced by:  1no  27827  0lt1s  27829  bday1  27831  cuteq0  27832  cutneg  27833  cuteq1  27834  gt0ne0s  27835  made0  27880  right1s  27913  0elold  27927  addsrid  27981  addslid  27985  addsproplem2  27987  addsfo  28000  ltaddspos1d  28028  ltaddspos2d  28029  addsgt0d  28031  ltsp1d  28032  addsge01d  28033  neg0s  28043  neg1s  28044  negsproplem2  28046  negsproplem6  28050  negscl  28053  negsid  28058  negsdi  28067  lt0negs2d  28068  subsfo  28082  negsval2  28083  subsid1  28085  posdifsd  28115  ltsubsposd  28116  subsge0d  28117  muls01  28129  mulsrid  28130  mulsproplem2  28134  mulsproplem3  28135  mulsproplem4  28136  mulsproplem5  28137  mulsproplem6  28138  mulsproplem7  28139  mulsproplem8  28140  mulscl  28151  ltmuls  28153  lemulsd  28155  muls02  28158  mulsgt0  28161  mulsge0d  28163  ltmulnegs1d  28193  mulscan2d  28196  lemuls1ad  28199  ltmuls12ad  28200  muls0ord  28202  precsexlem8  28231  precsexlem9  28232  precsexlem11  28234  recsex  28236  abs0s  28259  abssnid  28260  absmuls  28261  abssge0  28262  absnegs  28264  leabss  28265  0ons  28273  peano5n0s  28336  n0ssno  28337  0n0s  28346  peano2n0s  28347  dfn0s2  28349  n0sind  28350  n0cut  28351  n0sge0  28355  nnsgt0  28356  elnns2  28358  nnsge1  28360  nnsrecgt0d  28368  seqn0sfn  28377  n0subs  28380  n0lts1e0  28385  eucliddivs  28393  elzs2  28416  elnnzs  28418  elznns  28419  twocut  28440  nohalf  28441  pw2recs  28455  pw2gt0divsd  28462  pw2ge0divsd  28463  pw2divsnegd  28466  pw2divs0d  28472  halfcut  28475  bdaypw2n0bndlem  28480  bdaypw2n0bnd  28481  bdayfinbndlem1  28484  z12bdaylem1  28487  z12bday  28502  bdayfin  28504  recut  28511  elreno2  28512  0reno  28513  1reno  28514