Metamath Proof Explorer

Theorem 1n0

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

Ref Expression
Assertion 1n0 
|- 1o =/= (/)

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 nsuceq0 
 |-  suc (/) =/= (/)
3 1 2 eqnetri 
 |-  1o =/= (/)