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