This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0sdom1domALT

Description: Alternate proof of 0sdom1dom , shorter but requiring ax-un . (Contributed by NM, 28-Sep-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 0sdom1domALT ⊢ ∅ ≺ A ↔ 1 𝑜 ≼ A

Proof

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