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