Theorem sucdom

Description: Strict dominance of a set over a natural number is the same as dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013)

	Ref	Expression
Assertion	sucdom	|- ( 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 ) )