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 \in ω \to A ≺ suc A$

Proof

Step	Hyp	Ref	Expression
1		sucidg	$⊢ A \in ω \to A \in suc A$
2		nnord	$⊢ A \in ω \to Ord A$
3		ordsuc	$⊢ Ord A \leftrightarrow Ord suc A$
4	3	biimpi	$⊢ Ord A \to Ord suc A$
5		ordelpss	$⊢ (Ord A \land Ord suc A) \to (A \in suc A \leftrightarrow A \subset suc A)$
6	2 4 5	syl2anc2	$⊢ A \in ω \to (A \in suc A \leftrightarrow A \subset suc A)$
7	1 6	mpbid	$⊢ A \in ω \to A \subset suc A$
8		peano2b	$⊢ A \in ω \leftrightarrow suc A \in ω$
9		php2	$⊢ (suc A \in ω \land A \subset suc A) \to A ≺ suc A$
10	8 9	sylanb	$⊢ (A \in ω \land A \subset suc A) \to A ≺ suc A$
11	7 10	mpdan	$⊢ A \in ω \to A ≺ suc A$