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