Theorem 1sno 27776

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 27774	. 2 ⊢ 1s = ({ 0s } |s ∅)
2		0sno 27775	. . . . 5 ⊢ 0s ∈ No
3		snelpwi 5398	. . . . 5 ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
4	2, 3	ax-mp 5	. . . 4 ⊢ { 0s } ∈ 𝒫 No
5		nulssgt 27744	. . . 4 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
6	4, 5	ax-mp 5	. . 3 ⊢ { 0s } <<s ∅
7		scutcl 27748	. . 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 4292  𝒫 cpw 4559  {csn 4585   class class class wbr 5102  (class class class)co 7369   No csur 27584   <<s csslt 27726   |s cscut 27728   0_s c0s 27771   1_s c1s 27772

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 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

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 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-int 4907  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6323  df-on 6324  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-1o 8411  df-2o 8412  df-no 27587  df-slt 27588  df-bday 27589  df-sslt 27727  df-scut 27729  df-0s 27773  df-1s 27774

This theorem is referenced by:  cuteq1  27783  right1s  27845  peano2no  27931  sltp1d  27962  negs1s  27973  sltm1d  28045  mulsrid  28056  mulslid  28085  divs1  28147  precsexlem8  28156  precsexlem9  28157  precsexlem10  28158  precsexlem11  28159  divsrecd  28176  divsdird  28177  1ons  28198  n0scut  28266  n0scut2  28267  n0ons  28268  n0sge0  28270  n0s0suc  28274  nnsge1  28275  n0addscl  28276  n0mulscl  28277  1n0s  28280  nnsrecgt0d  28283  n0sfincut  28286  n0s0m1  28292  n0subs  28293  n0sltp1le  28295  n0sleltp1  28296  n0slem1lt  28297  n0p1nns  28300  dfnns2  28301  nnsind  28302  nn1m1nns  28303  nnm1n0s  28304  eucliddivs  28305  nnzs  28314  0zs  28316  elzn0s  28326  peano5uzs  28332  zscut  28335  1p1e2s  28343  no2times  28344  n0seo  28348  zseo  28349  twocut  28350  nohalf  28351  expsval  28352  exps1  28355  expsp1  28356  expscl  28358  expadds  28362  pw2recs  28365  pw2divsrecd  28374  pw2divsdird  28375  halfcut  28381  addhalfcut  28382  pw2cut  28383  pw2cutp1  28384  zs12bday  28396  recut  28400  0reno  28401  renegscl  28402  readdscl  28403  remulscllem1  28404  remulscl  28406