Theorem 0no 28225

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 28223	. 2 ⊢ 0s = (∅ |s ∅)
2		0elpw 5321	. . . 4 ⊢ ∅ ∈ 𝒫 No
3		nulsgts 28192	. . . 4 ⊢ (∅ ∈ 𝒫 No → ∅ <<s ∅)
4	2, 3	ax-mp 5	. . 3 ⊢ ∅ <<s ∅
5		cutscl 28198	. . 3 ⊢ (∅ <<s ∅ → (∅ |s ∅) ∈ No)
6	4, 5	ax-mp 5	. 2 ⊢ (∅ |s ∅) ∈ No
7	1, 6	eqeltri 2860	1 ⊢ 0s ∈ No

This proof depends on syntax axioms:   ∈ wcel 2147  ∅c0 4281  𝒫 cpw 4560   class class class wbr 5106  (class class class)co 7443  Nocsur 28027   <<s cslts 28173   |s ccuts 28175   0_s c0s 28221

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6383  df-on 6384  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-1o 8504  df-2o 8505  df-no 28030  df-lts 28031  df-bday 28032  df-slts 28174  df-cuts 28176  df-0s 28223

This theorem is used by:  1no  28226  0lt1s  28228  bday1  28230  cuteq0  28231  cutneg  28232  cuteq1  28233  gt0ne0s  28234  made0  28279  right1s  28312  0elold  28326  addsrid  28380  addslid  28384  addsproplem2  28386  addsfo  28399  ltaddspos1d  28427  ltaddspos2d  28428  addsgt0d  28430  ltsp1d  28431  addsge01d  28432  neg0s  28442  neg1s  28443  negsproplem2  28445  negsproplem6  28449  negscl  28452  negsid  28457  negsdi  28466  lt0negs2d  28467  subsfo  28481  negsval2  28482  subsid1  28484  posdifsd  28514  ltsubsposd  28515  subsge0d  28516  muls01  28528  mulsrid  28529  mulsproplem2  28533  mulsproplem3  28534  mulsproplem4  28535  mulsproplem5  28536  mulsproplem6  28537  mulsproplem7  28538  mulsproplem8  28539  mulscl  28550  ltmuls  28552  lemulsd  28554  muls02  28557  mulsgt0  28560  mulsge0d  28562  ltmulnegs1d  28592  mulscan2d  28595  lemuls1ad  28598  ltmuls12ad  28599  muls0ord  28601  precsexlem8  28630  precsexlem9  28631  precsexlem11  28633  recsex  28635  abs0s  28658  abssnid  28659  absmuls  28660  abssge0  28661  absnegs  28663  leabss  28664  0ons  28672  peano5n0s  28735  n0ssno  28736  0n0s  28745  peano2n0s  28746  dfn0s2  28748  n0sind  28749  n0cut  28750  n0sge0  28754  nnsgt0  28755  elnns2  28757  nnsge1  28759  nnsrecgt0d  28767  seqn0sfn  28776  n0subs  28779  n0lts1e0  28784  eucliddivs  28792  elzs2  28815  elnnzs  28817  elznns  28818  twocut  28839  nohalf  28840  pw2recs  28854  pw2gt0divsd  28861  pw2ge0divsd  28862  pw2divsnegd  28865  pw2divs0d  28871  halfcut  28874  bdaypw2n0bndlem  28879  bdaypw2n0bnd  28880  bdayfinbndlem1  28883  z12bdaylem1  28886  z12bday  28901  bdayfin  28903  recut  28910  elreno2  28911  0reno  28912  1reno  28913