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 |
| 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 |