Theorem php4

Description: Corollary of the Pigeonhole Principle php : a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004)

	Ref	Expression
Assertion	php4	|- ( A e. _om -> A ~< suc A )

Proof

Step	Hyp	Ref	Expression
1		sucidg	|- ( A e. _om -> A e. suc A )
2		nnord	|- ( A e. _om -> Ord A )
3		ordsuc	|- ( Ord A <-> Ord suc A )
4	3	biimpi	|- ( Ord A -> Ord suc A )
5		ordelpss	|- ( ( Ord A /\ Ord suc A ) -> ( A e. suc A <-> A C. suc A ) )
6	2 4 5	syl2anc2	|- ( A e. _om -> ( A e. suc A <-> A C. suc A ) )
7	1 6	mpbid	|- ( A e. _om -> A C. suc A )
8		peano2b	|- ( A e. _om <-> suc A e. _om )
9		php2	|- ( ( suc A e. _om /\ A C. suc A ) -> A ~< suc A )
10	8 9	sylanb	|- ( ( A e. _om /\ A C. suc A ) -> A ~< suc A )
11	7 10	mpdan	|- ( A e. _om -> A ~< suc A )