Metamath Proof Explorer


Theorem sucdomOLD

Description: Obsolete version of sucdom as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sucdomOLD
|- ( A e. _om -> ( A ~< B <-> suc A ~<_ B ) )

Proof

Step Hyp Ref Expression
1 sucdom2
 |-  ( A ~< B -> suc A ~<_ B )
2 php4
 |-  ( A e. _om -> A ~< suc A )
3 sdomdomtr
 |-  ( ( A ~< suc A /\ suc A ~<_ B ) -> A ~< B )
4 3 ex
 |-  ( A ~< suc A -> ( suc A ~<_ B -> A ~< B ) )
5 2 4 syl
 |-  ( A e. _om -> ( suc A ~<_ B -> A ~< B ) )
6 1 5 impbid2
 |-  ( A e. _om -> ( A ~< B <-> suc A ~<_ B ) )