Theorem 0no 27821

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

Syntax hints:   ∈ wcel 2121  ∅c0 4263  𝒫 cpw 4531   class class class wbr 5074  (class class class)co 7359   No csur 27624   <<s cslts 27769   |s ccuts 27771   0_s c0s 27817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7681

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3904  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4841  df-int 4880  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-ord 6316  df-on 6317  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7316  df-ov 7362  df-oprab 7363  df-mpo 7364  df-1o 8399  df-2o 8400  df-no 27627  df-lts 27628  df-bday 27629  df-slts 27770  df-cuts 27772  df-0s 27819

This theorem is referenced by:  1no  27822  0lt1s  27824  bday1  27826  cuteq0  27827  cutneg  27828  cuteq1  27829  gt0ne0s  27830  made0  27875  right1s  27908  0elold  27922  addsrid  27976  addslid  27980  addsproplem2  27982  addsfo  27995  ltaddspos1d  28023  ltaddspos2d  28024  addsgt0d  28026  ltsp1d  28027  addsge01d  28028  neg0s  28038  neg1s  28039  negsproplem2  28041  negsproplem6  28045  negscl  28048  negsid  28053  negsdi  28062  lt0negs2d  28063  subsfo  28077  negsval2  28078  subsid1  28080  posdifsd  28110  ltsubsposd  28111  subsge0d  28112  muls01  28124  mulsrid  28125  mulsproplem2  28129  mulsproplem3  28130  mulsproplem4  28131  mulsproplem5  28132  mulsproplem6  28133  mulsproplem7  28134  mulsproplem8  28135  mulscl  28146  ltmuls  28148  lemulsd  28150  muls02  28153  mulsgt0  28156  mulsge0d  28158  ltmulnegs1d  28188  mulscan2d  28191  lemuls1ad  28194  ltmuls12ad  28195  muls0ord  28197  precsexlem8  28226  precsexlem9  28227  precsexlem11  28229  recsex  28231  abs0s  28254  abssnid  28255  absmuls  28256  abssge0  28257  absnegs  28259  leabss  28260  0ons  28268  peano5n0s  28331  n0ssno  28332  0n0s  28341  peano2n0s  28342  dfn0s2  28344  n0sind  28345  n0cut  28346  n0sge0  28350  nnsgt0  28351  elnns2  28353  nnsge1  28355  nnsrecgt0d  28363  seqn0sfn  28372  n0subs  28375  n0lts1e0  28380  eucliddivs  28388  elzs2  28411  elnnzs  28413  elznns  28414  twocut  28435  nohalf  28436  pw2recs  28450  pw2gt0divsd  28457  pw2ge0divsd  28458  pw2divsnegd  28461  pw2divs0d  28467  halfcut  28470  bdaypw2n0bndlem  28475  bdaypw2n0bnd  28476  bdayfinbndlem1  28479  z12bdaylem1  28482  z12bday  28497  bdayfin  28499  recut  28506  elreno2  28507  0reno  28508  1reno  28509