Theorem 0no 27815

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 27813	. 2 ⊢ 0s = (∅ |s ∅)
2		0elpw 5293	. . . 4 ⊢ ∅ ∈ 𝒫 No
3		nulsgts 27782	. . . 4 ⊢ (∅ ∈ 𝒫 No → ∅ <<s ∅)
4	2, 3	ax-mp 5	. . 3 ⊢ ∅ <<s ∅
5		cutscl 27788	. . 3 ⊢ (∅ <<s ∅ → (∅ |s ∅) ∈ No )
6	4, 5	ax-mp 5	. 2 ⊢ (∅ |s ∅) ∈ No
7	1, 6	eqeltri 2833	1 ⊢ 0s ∈ No

Syntax hints:   ∈ wcel 2114  ∅c0 4274  𝒫 cpw 4542   class class class wbr 5086  (class class class)co 7360   No csur 27617   <<s cslts 27763   |s ccuts 27765   0_s c0s 27811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  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 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1o 8398  df-2o 8399  df-no 27620  df-lts 27621  df-bday 27622  df-slts 27764  df-cuts 27766  df-0s 27813

This theorem is referenced by:  1no  27816  0lt1s  27818  bday1  27820  cuteq0  27821  cutneg  27822  cuteq1  27823  gt0ne0s  27824  made0  27869  right1s  27902  0elold  27916  addsrid  27970  addslid  27974  addsproplem2  27976  addsfo  27989  ltaddspos1d  28017  ltaddspos2d  28018  addsgt0d  28020  ltsp1d  28021  addsge01d  28022  neg0s  28032  neg1s  28033  negsproplem2  28035  negsproplem6  28039  negscl  28042  negsid  28047  negsdi  28056  lt0negs2d  28057  subsfo  28071  negsval2  28072  subsid1  28074  posdifsd  28104  ltsubsposd  28105  subsge0d  28106  muls01  28118  mulsrid  28119  mulsproplem2  28123  mulsproplem3  28124  mulsproplem4  28125  mulsproplem5  28126  mulsproplem6  28127  mulsproplem7  28128  mulsproplem8  28129  mulscl  28140  ltmuls  28142  lemulsd  28144  muls02  28147  mulsgt0  28150  mulsge0d  28152  ltmulnegs1d  28182  mulscan2d  28185  lemuls1ad  28188  ltmuls12ad  28189  muls0ord  28191  precsexlem8  28220  precsexlem9  28221  precsexlem11  28223  recsex  28225  abs0s  28248  abssnid  28249  absmuls  28250  abssge0  28251  absnegs  28253  leabss  28254  0ons  28262  peano5n0s  28325  n0ssno  28326  0n0s  28335  peano2n0s  28336  dfn0s2  28338  n0sind  28339  n0cut  28340  n0sge0  28344  nnsgt0  28345  elnns2  28347  nnsge1  28349  nnsrecgt0d  28357  seqn0sfn  28366  n0subs  28369  n0lts1e0  28374  eucliddivs  28382  elzs2  28405  elnnzs  28407  elznns  28408  twocut  28429  nohalf  28430  pw2recs  28444  pw2gt0divsd  28451  pw2ge0divsd  28452  pw2divsnegd  28455  pw2divs0d  28461  halfcut  28464  bdaypw2n0bndlem  28469  bdaypw2n0bnd  28470  bdayfinbndlem1  28473  z12bdaylem1  28476  z12bday  28491  bdayfin  28493  recut  28500  elreno2  28501  0reno  28502  1reno  28503