Metamath Proof Explorer


Theorem 0lt1o

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

Ref Expression
Assertion 0lt1o 1 𝑜

Proof

Step Hyp Ref Expression
1 eqid =
2 el1o 1 𝑜 =
3 1 2 mpbir 1 𝑜