Metamath Proof Explorer
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 ≼ 𝐴 ) |