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	⊢ ( 𝐴 ∈ ω → 𝐴 ≺ suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		sucidg	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ suc 𝐴 )
2		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
3		ordsuc	⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
4	3	biimpi	⊢ ( Ord 𝐴 → Ord suc 𝐴 )
5		ordelpss	⊢ ( ( Ord 𝐴 ∧ Ord suc 𝐴 ) → ( 𝐴 ∈ suc 𝐴 ↔ 𝐴 ⊊ suc 𝐴 ) )
6	2 4 5	syl2anc2	⊢ ( 𝐴 ∈ ω → ( 𝐴 ∈ suc 𝐴 ↔ 𝐴 ⊊ suc 𝐴 ) )
7	1 6	mpbid	⊢ ( 𝐴 ∈ ω → 𝐴 ⊊ suc 𝐴 )
8		peano2b	⊢ ( 𝐴 ∈ ω ↔ suc 𝐴 ∈ ω )
9		php2	⊢ ( ( suc 𝐴 ∈ ω ∧ 𝐴 ⊊ suc 𝐴 ) → 𝐴 ≺ suc 𝐴 )
10	8 9	sylanb	⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ⊊ suc 𝐴 ) → 𝐴 ≺ suc 𝐴 )
11	7 10	mpdan	⊢ ( 𝐴 ∈ ω → 𝐴 ≺ suc 𝐴 )