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 1 𝑜 2 𝑜

Proof

Step Hyp Ref Expression
1 2on0 2 𝑜
2 2oex 2 𝑜 V
3 2 0sdom 2 𝑜 2 𝑜
4 1 3 mpbir 2 𝑜
5 0sdom1dom 2 𝑜 1 𝑜 2 𝑜
6 4 5 mpbi 1 𝑜 2 𝑜
7 snnen2o ¬ 2 𝑜
8 df1o2 1 𝑜 =
9 8 breq1i 1 𝑜 2 𝑜 2 𝑜
10 7 9 mtbir ¬ 1 𝑜 2 𝑜
11 brsdom 1 𝑜 2 𝑜 1 𝑜 2 𝑜 ¬ 1 𝑜 2 𝑜
12 6 10 11 mpbir2an 1 𝑜 2 𝑜