Theorem 1sno 27741

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

Assertion

Ref	Expression
1sno	⊢ 1s ∈ No

Proof of Theorem 1sno

Step	Hyp	Ref	Expression
1		df-1s 27739	. 2 ⊢ 1s = ({ 0s } |s ∅)
2		0sno 27740	. . . . 5 ⊢ 0s ∈ No
3		snelpwi 5386	. . . . 5 ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
4	2, 3	ax-mp 5	. . . 4 ⊢ { 0s } ∈ 𝒫 No
5		nulssgt 27709	. . . 4 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
6	4, 5	ax-mp 5	. . 3 ⊢ { 0s } <<s ∅
7		scutcl 27713	. . 3 ⊢ ({ 0s } <<s ∅ → ({ 0s } |s ∅) ∈ No )
8	6, 7	ax-mp 5	. 2 ⊢ ({ 0s } |s ∅) ∈ No
9	1, 8	eqeltri 2824	1 ⊢ 1s ∈ No

Syntax hints:   ∈ wcel 2109  ∅c0 4284  𝒫 cpw 4551  {csn 4577   class class class wbr 5092  (class class class)co 7349   No csur 27549   <<s csslt 27691   |s cscut 27693   0_s c0s 27736   1_s c1s 27737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4859  df-int 4897  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6310  df-on 6311  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-1o 8388  df-2o 8389  df-no 27552  df-slt 27553  df-bday 27554  df-sslt 27692  df-scut 27694  df-0s 27738  df-1s 27739

This theorem is referenced by:  cuteq1  27748  right1s  27810  peano2no  27896  sltp1d  27927  negs1s  27938  sltm1d  28010  mulsrid  28021  mulslid  28050  divs1  28112  precsexlem8  28121  precsexlem9  28122  precsexlem10  28123  precsexlem11  28124  divsrecd  28141  divsdird  28142  1ons  28163  n0scut  28231  n0scut2  28232  n0ons  28233  n0sge0  28235  n0s0suc  28239  nnsge1  28240  n0addscl  28241  n0mulscl  28242  1n0s  28245  nnsrecgt0d  28248  n0sfincut  28251  n0s0m1  28257  n0subs  28258  n0sltp1le  28260  n0sleltp1  28261  n0slem1lt  28262  n0p1nns  28265  dfnns2  28266  nnsind  28267  nn1m1nns  28268  nnm1n0s  28269  eucliddivs  28270  nnzs  28279  0zs  28281  elzn0s  28291  peano5uzs  28297  zscut  28300  1p1e2s  28308  no2times  28309  n0seo  28313  zseo  28314  twocut  28315  nohalf  28316  expsval  28317  exps1  28320  expsp1  28321  expscl  28323  expadds  28327  pw2recs  28330  pw2divsrecd  28339  pw2divsdird  28340  halfcut  28346  addhalfcut  28347  pw2cut  28348  pw2cutp1  28349  zs12bday  28361  recut  28365  0reno  28366  renegscl  28367  readdscl  28368  remulscllem1  28369  remulscl  28371