Theorem 0no 28082

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 28080	. 2 ⊢ 0s = (∅ |s ∅)
2		0elpw 5324	. . . 4 ⊢ ∅ ∈ 𝒫 No
3		nulsgts 28049	. . . 4 ⊢ (∅ ∈ 𝒫 No → ∅ <<s ∅)
4	2, 3	ax-mp 5	. . 3 ⊢ ∅ <<s ∅
5		cutscl 28055	. . 3 ⊢ (∅ <<s ∅ → (∅ |s ∅) ∈ No )
6	4, 5	ax-mp 5	. 2 ⊢ (∅ |s ∅) ∈ No
7	1, 6	eqeltri 2858	1 ⊢ 0s ∈ No

This proof depends on syntax axioms:   ∈ wcel 2145  ∅c0 4282  𝒫 cpw 4560   class class class wbr 5107  (class class class)co 7417   No csur 27884   <<s cslts 28030   |s ccuts 28032   0_s c0s 28078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  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 6364  df-on 6365  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-1o 8459  df-2o 8460  df-no 27887  df-lts 27888  df-bday 27889  df-slts 28031  df-cuts 28033  df-0s 28080

This theorem is used by:  1no  28083  0lt1s  28085  bday1  28087  cuteq0  28088  cutneg  28089  cuteq1  28090  gt0ne0s  28091  made0  28136  right1s  28169  0elold  28183  addsrid  28237  addslid  28241  addsproplem2  28243  addsfo  28256  ltaddspos1d  28284  ltaddspos2d  28285  addsgt0d  28287  ltsp1d  28288  addsge01d  28289  neg0s  28299  neg1s  28300  negsproplem2  28302  negsproplem6  28306  negscl  28309  negsid  28314  negsdi  28323  lt0negs2d  28324  subsfo  28338  negsval2  28339  subsid1  28341  posdifsd  28371  ltsubsposd  28372  subsge0d  28373  muls01  28385  mulsrid  28386  mulsproplem2  28390  mulsproplem3  28391  mulsproplem4  28392  mulsproplem5  28393  mulsproplem6  28394  mulsproplem7  28395  mulsproplem8  28396  mulscl  28407  ltmuls  28409  lemulsd  28411  muls02  28414  mulsgt0  28417  mulsge0d  28419  ltmulnegs1d  28449  mulscan2d  28452  lemuls1ad  28455  ltmuls12ad  28456  muls0ord  28458  precsexlem8  28487  precsexlem9  28488  precsexlem11  28490  recsex  28492  abs0s  28515  abssnid  28516  absmuls  28517  abssge0  28518  absnegs  28520  leabss  28521  0ons  28529  peano5n0s  28592  n0ssno  28593  0n0s  28602  peano2n0s  28603  dfn0s2  28605  n0sind  28606  n0cut  28607  n0sge0  28611  nnsgt0  28612  elnns2  28614  nnsge1  28616  nnsrecgt0d  28624  seqn0sfn  28633  n0subs  28636  n0lts1e0  28641  eucliddivs  28649  elzs2  28672  elnnzs  28674  elznns  28675  twocut  28696  nohalf  28697  pw2recs  28711  pw2gt0divsd  28718  pw2ge0divsd  28719  pw2divsnegd  28722  pw2divs0d  28728  halfcut  28731  bdaypw2n0bndlem  28736  bdaypw2n0bnd  28737  bdayfinbndlem1  28740  z12bdaylem1  28743  z12bday  28758  bdayfin  28760  recut  28767  elreno2  28768  0reno  28769  1reno  28770