Metamath Proof Explorer

Theorem 0lt1o

Description: Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005)

Ref Expression
Assertion 0lt1o 
|- (/) e. 1o

Proof

Step Hyp Ref Expression
1 eqid 
 |-  (/) = (/)
2 el1o 
 |-  ( (/) e. 1o <-> (/) = (/) )
3 1 2 mpbir 
 |-  (/) e. 1o