Metamath Proof Explorer

Theorem 1sdom2

Description: Ordinal 1 is strictly dominated by ordinal 2. (Contributed by NM, 4-Apr-2007)

Ref Expression
Assertion 1sdom2 
|- 1o ~< 2o

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 php4 
 |-  ( 1o e. _om -> 1o ~< suc 1o )
3 1 2 ax-mp 
 |-  1o ~< suc 1o
4 df-2o 
 |-  2o = suc 1o
5 3 4 breqtrri 
 |-  1o ~< 2o