Metamath Proof Explorer


Theorem 1sdom2

Description: Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un , see 1sdom2ALT . (Contributed by NM, 4-Apr-2007) Avoid ax-un . (Revised by BTernaryTau, 8-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 2on0
 |-  2o =/= (/)
2 2oex
 |-  2o e. _V
3 2 0sdom
 |-  ( (/) ~< 2o <-> 2o =/= (/) )
4 1 3 mpbir
 |-  (/) ~< 2o
5 0sdom1dom
 |-  ( (/) ~< 2o <-> 1o ~<_ 2o )
6 4 5 mpbi
 |-  1o ~<_ 2o
7 snnen2o
 |-  -. { (/) } ~~ 2o
8 df1o2
 |-  1o = { (/) }
9 8 breq1i
 |-  ( 1o ~~ 2o <-> { (/) } ~~ 2o )
10 7 9 mtbir
 |-  -. 1o ~~ 2o
11 brsdom
 |-  ( 1o ~< 2o <-> ( 1o ~<_ 2o /\ -. 1o ~~ 2o ) )
12 6 10 11 mpbir2an
 |-  1o ~< 2o