| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 2on0 | Structured version Visualization version GIF version | ||
| Description: Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
| Ref | Expression |
|---|---|
| 2on0 | ⊢ 2o ≠ ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-2o 8507 | . 2 ⊢ 2o = suc 1o | |
| 2 | nsuceq0 6467 | . 2 ⊢ suc 1o ≠ ∅ | |
| 3 | 1, 2 | eqnetri 3011 | 1 ⊢ 2o ≠ ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: ≠ wne 2940 ∅c0 4333 suc csuc 6386 1oc1o 8499 2oc2o 8500 |
| 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-ext 2708 ax-nul 5306 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-v 3482 df-dif 3954 df-un 3956 df-nul 4334 df-sn 4627 df-suc 6390 df-2o 8507 |
| This theorem is referenced by: ord2eln012 8535 snnen2oOLD 9264 snnen2o 9273 1sdom2 9276 1sdom2dom 9283 pmtrfmvdn0 19480 pmtrsn 19537 efgrcl 19733 sltval2 27701 sltintdifex 27706 nogt01o 27741 noinfbnd1lem5 27772 noinfbnd2lem1 27775 goaln0 35398 goalr 35402 fmla0disjsuc 35403 onint1 36450 1oequni2o 37369 finxpreclem4 37395 finxp3o 37401 frlmpwfi 43110 clsk1indlem1 44058 |
| Copyright terms: Public domain | W3C validator |