Metamath Proof Explorer


Theorem 1sdom2ALT

Description: Alternate proof of 1sdom2 , shorter but requiring ax-un . (Contributed by NM, 4-Apr-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 1sdom2ALT 1o ≺ 2o

Proof

Step Hyp Ref Expression
1 1onn 1o ∈ ω
2 php4 ( 1o ∈ ω → 1o ≺ suc 1o )
3 1 2 ax-mp 1o ≺ suc 1o
4 df-2o 2o = suc 1o
5 3 4 breqtrri 1o ≺ 2o