Metamath Proof Explorer

Theorem 1one2o

Description: Ordinal one is not ordinal two. Analogous to 1ne2 . (Contributed by AV, 17-Oct-2023)

Ref Expression
Assertion 1one2o 
|- 1o =/= 2o

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 omsucne 
 |-  ( 1o e. _om -> 1o =/= suc 1o )
3 1 2 ax-mp 
 |-  1o =/= suc 1o
4 df-2o 
 |-  2o = suc 1o
5 3 4 neeqtrri 
 |-  1o =/= 2o