| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 0sno | Structured version Visualization version GIF version | ||
| Description: Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
| Ref | Expression |
|---|---|
| 0sno | ⊢ 0s ∈ No |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-0s 27869 | . 2 ⊢ 0s = (∅ |s ∅) | |
| 2 | 0elpw 5356 | . . . 4 ⊢ ∅ ∈ 𝒫 No | |
| 3 | nulssgt 27843 | . . . 4 ⊢ (∅ ∈ 𝒫 No → ∅ <<s ∅) | |
| 4 | 2, 3 | ax-mp 5 | . . 3 ⊢ ∅ <<s ∅ |
| 5 | scutcl 27847 | . . 3 ⊢ (∅ <<s ∅ → (∅ |s ∅) ∈ No ) | |
| 6 | 4, 5 | ax-mp 5 | . 2 ⊢ (∅ |s ∅) ∈ No |
| 7 | 1, 6 | eqeltri 2837 | 1 ⊢ 0s ∈ No |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 ∅c0 4333 𝒫 cpw 4600 class class class wbr 5143 (class class class)co 7431 No csur 27684 <<s csslt 27825 |s cscut 27827 0s c0s 27867 |
| 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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-ord 6387 df-on 6388 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-1o 8506 df-2o 8507 df-no 27687 df-slt 27688 df-bday 27689 df-sslt 27826 df-scut 27828 df-0s 27869 |
| This theorem is referenced by: 1sno 27872 0slt1s 27874 bday1s 27876 cuteq0 27877 cuteq1 27878 sgt0ne0 27879 made0 27912 right1s 27934 0elold 27947 addsrid 27997 addslid 28001 addsproplem2 28003 addsfo 28016 sltaddpos1d 28044 sltaddpos2d 28045 addsgt0d 28047 sltp1d 28048 negs0s 28058 negs1s 28059 negsproplem2 28061 negsproplem6 28065 negscl 28068 negsid 28073 negsdi 28082 slt0neg2d 28083 subsfo 28095 negsval2 28096 subsid1 28098 posdifsd 28127 sltsubposd 28128 subsge0d 28129 muls01 28138 mulsrid 28139 mulsproplem2 28143 mulsproplem3 28144 mulsproplem4 28145 mulsproplem5 28146 mulsproplem6 28147 mulsproplem7 28148 mulsproplem8 28149 mulscl 28160 sltmul 28162 slemuld 28164 muls02 28167 mulsgt0 28170 mulsge0d 28172 sltmulneg1d 28202 mulscan2d 28205 slemul1ad 28208 sltmul12ad 28209 muls0ord 28211 precsexlem8 28238 precsexlem9 28239 precsexlem11 28241 recsex 28243 abs0s 28266 abssnid 28267 absmuls 28268 abssge0 28269 abssneg 28271 sleabs 28272 0ons 28279 om2noseqlt 28305 peano5n0s 28324 n0ssno 28325 0n0s 28334 peano2n0s 28335 dfn0s2 28336 n0sind 28337 n0scut 28338 n0sge0 28341 nnsgt0 28342 elnns2 28344 nnsge1 28346 nnsrecgt0d 28356 seqn0sfn 28357 n0subs 28360 elzs2 28385 elnnzs 28387 elznns 28388 1p1e2s 28400 nohalf 28407 cutpw2 28417 pw2bday 28418 recut 28428 0reno 28429 |
| Copyright terms: Public domain | W3C validator |