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 <-> 1o ~<_ A )

Proof

Step Hyp Ref Expression
1 peano1
 |-  (/) e. _om
2 sucdom
 |-  ( (/) e. _om -> ( (/) ~< A <-> suc (/) ~<_ A ) )
3 1 2 ax-mp
 |-  ( (/) ~< A <-> suc (/) ~<_ A )
4 df-1o
 |-  1o = suc (/)
5 4 breq1i
 |-  ( 1o ~<_ A <-> suc (/) ~<_ A )
6 3 5 bitr4i
 |-  ( (/) ~< A <-> 1o ~<_ A )