Metamath Proof Explorer


Theorem 0sdom1dom

Description: Strict dominance over zero is the same as dominance over one. (Contributed by NM, 28-Sep-2004)

Ref Expression
Assertion 0sdom1dom ( ∅ ≺ 𝐴 ↔ 1o𝐴 )

Proof

Step Hyp Ref Expression
1 peano1 ∅ ∈ ω
2 sucdom ( ∅ ∈ ω → ( ∅ ≺ 𝐴 ↔ suc ∅ ≼ 𝐴 ) )
3 1 2 ax-mp ( ∅ ≺ 𝐴 ↔ suc ∅ ≼ 𝐴 )
4 df-1o 1o = suc ∅
5 4 breq1i ( 1o𝐴 ↔ suc ∅ ≼ 𝐴 )
6 3 5 bitr4i ( ∅ ≺ 𝐴 ↔ 1o𝐴 )