This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )