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 ω A suc A

Proof

Step Hyp Ref Expression
1 sucidg A ω A suc A
2 nnord A ω 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 suc A A suc A
6 2 4 5 syl2anc2 A ω A suc A A suc A
7 1 6 mpbid A ω A suc A
8 peano2b A ω suc A ω
9 php2 suc A ω A suc A A suc A
10 8 9 sylanb A ω A suc A A suc A
11 7 10 mpdan A ω A suc A