Theorem 0no 28039

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 28037	. 2 ⊢ 0s = (∅ |s ∅)
2		0elpw 5331	. . . 4 ⊢ ∅ ∈ 𝒫 No
3		nulsgts 28006	. . . 4 ⊢ (∅ ∈ 𝒫 No → ∅ <<s ∅)
4	2, 3	ax-mp 5	. . 3 ⊢ ∅ <<s ∅
5		cutscl 28012	. . 3 ⊢ (∅ <<s ∅ → (∅ |s ∅) ∈ No )
6	4, 5	ax-mp 5	. 2 ⊢ (∅ |s ∅) ∈ No
7	1, 6	eqeltri 2862	1 ⊢ 0s ∈ No

This proof depends on syntax axioms:   ∈ wcel 2146  ∅c0 4289  𝒫 cpw 4567   class class class wbr 5114  (class class class)co 7423   No csur 27841   <<s cslts 27987   |s ccuts 27989   0_s c0s 28035

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4878  df-int 4918  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-ord 6370  df-on 6371  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-1o 8462  df-2o 8463  df-no 27844  df-lts 27845  df-bday 27846  df-slts 27988  df-cuts 27990  df-0s 28037

This theorem is used by:  1no  28040  0lt1s  28042  bday1  28044  cuteq0  28045  cutneg  28046  cuteq1  28047  gt0ne0s  28048  made0  28093  right1s  28126  0elold  28140  addsrid  28194  addslid  28198  addsproplem2  28200  addsfo  28213  ltaddspos1d  28241  ltaddspos2d  28242  addsgt0d  28244  ltsp1d  28245  addsge01d  28246  neg0s  28256  neg1s  28257  negsproplem2  28259  negsproplem6  28263  negscl  28266  negsid  28271  negsdi  28280  lt0negs2d  28281  subsfo  28295  negsval2  28296  subsid1  28298  posdifsd  28328  ltsubsposd  28329  subsge0d  28330  muls01  28342  mulsrid  28343  mulsproplem2  28347  mulsproplem3  28348  mulsproplem4  28349  mulsproplem5  28350  mulsproplem6  28351  mulsproplem7  28352  mulsproplem8  28353  mulscl  28364  ltmuls  28366  lemulsd  28368  muls02  28371  mulsgt0  28374  mulsge0d  28376  ltmulnegs1d  28406  mulscan2d  28409  lemuls1ad  28412  ltmuls12ad  28413  muls0ord  28415  precsexlem8  28444  precsexlem9  28445  precsexlem11  28447  recsex  28449  abs0s  28472  abssnid  28473  absmuls  28474  abssge0  28475  absnegs  28477  leabss  28478  0ons  28486  peano5n0s  28549  n0ssno  28550  0n0s  28559  peano2n0s  28560  dfn0s2  28562  n0sind  28563  n0cut  28564  n0sge0  28568  nnsgt0  28569  elnns2  28571  nnsge1  28573  nnsrecgt0d  28581  seqn0sfn  28590  n0subs  28593  n0lts1e0  28598  eucliddivs  28606  elzs2  28629  elnnzs  28631  elznns  28632  twocut  28653  nohalf  28654  pw2recs  28668  pw2gt0divsd  28675  pw2ge0divsd  28676  pw2divsnegd  28679  pw2divs0d  28685  halfcut  28688  bdaypw2n0bndlem  28693  bdaypw2n0bnd  28694  bdayfinbndlem1  28697  z12bdaylem1  28700  z12bday  28715  bdayfin  28717  recut  28724  elreno2  28725  0reno  28726  1reno  28727