Theorem 1no 27790

Description: Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)

Assertion

Ref	Expression
1no	⊢ 1s ∈ No

Proof of Theorem 1no

Step	Hyp	Ref	Expression
1		df-1s 27788	. 2 ⊢ 1s = ({ 0s } |s ∅)
2		0no 27789	. . . . 5 ⊢ 0s ∈ No
3		snelpwi 5389	. . . . 5 ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
4	2, 3	ax-mp 5	. . . 4 ⊢ { 0s } ∈ 𝒫 No
5		nulsgts 27756	. . . 4 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
6	4, 5	ax-mp 5	. . 3 ⊢ { 0s } <<s ∅
7		cutscl 27762	. . 3 ⊢ ({ 0s } <<s ∅ → ({ 0s } |s ∅) ∈ No )
8	6, 7	ax-mp 5	. 2 ⊢ ({ 0s } |s ∅) ∈ No
9	1, 8	eqeltri 2833	1 ⊢ 1s ∈ No

Syntax hints:   ∈ wcel 2114  ∅c0 4274  𝒫 cpw 4542  {csn 4568   class class class wbr 5086  (class class class)co 7358   No csur 27591   <<s cslts 27737   |s ccuts 27739   0_s c0s 27785   1_s c1s 27786

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 5300  ax-pr 5368  ax-un 7680

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 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-ord 6318  df-on 6319  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1o 8396  df-2o 8397  df-no 27594  df-lts 27595  df-bday 27596  df-slts 27738  df-cuts 27740  df-0s 27787  df-1s 27788

This theorem is referenced by:  cuteq1  27797  right1s  27876  peano2no  27964  ltsp1d  27995  neg1s  28007  ltsm1d  28082  mulsrid  28093  mulslid  28122  divs1  28184  precsexlem8  28194  precsexlem9  28195  precsexlem10  28196  precsexlem11  28197  divsrecd  28214  divsdird  28215  1ons  28237  n0cut  28314  n0cut2  28315  n0on  28316  n0sge0  28318  n0s0suc  28322  nnsge1  28323  n0addscl  28324  n0mulscl  28325  1n0s  28328  nnsrecgt0d  28331  n0fincut  28335  n0s0m1  28342  n0subs  28343  n0ltsp1le  28345  n0lesltp1  28346  n0lesm1lt  28347  n0lts1e0  28348  n0p1nns  28351  dfnns2  28352  nnsind  28353  nn1m1nns  28354  nnm1n0s  28355  eucliddivs  28356  nnzs  28366  0zs  28368  elzn0s  28378  peano5uzs  28384  zcuts  28387  no2times  28397  n0seo  28401  zseo  28402  twocut  28403  nohalf  28404  expsval  28405  exps1  28408  expsp1  28409  expscl  28411  expadds  28415  pw2recs  28418  pw2divsrecd  28427  pw2divsdird  28428  pw2divsidd  28436  halfcut  28438  addhalfcut  28439  pw2cut  28440  pw2cutp1  28441  pw2cut2  28442  bdaypw2n0bndlem  28443  bdaypw2bnd  28445  bdayfinbndlem1  28447  z12bdaylem1  28450  z12bdaylem2  28451  recut  28474  elreno2  28475  0reno  28476  1reno  28477  renegscl  28478  readdscl  28479  remulscllem1  28480  remulscl  28482