php2

Description: Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 20-Nov-2024)

		Ref	Expression
	Assertion	php2	$⊢ (A \in ω \land B \subset A) \to B ≺ A$

Step	Hyp	Ref	Expression
1		nnfi	$⊢ A \in ω \to A \in Fin$
2		pssss	$⊢ B \subset A \to B \subseteq A$
3		ssdomfi	$⊢ A \in Fin \to (B \subseteq A \to B ≼ A)$
4	3	imp	$⊢ (A \in Fin \land B \subseteq A) \to B ≼ A$
5	1 2 4	syl2an	$⊢ (A \in ω \land B \subset A) \to B ≼ A$
6		php	$⊢ (A \in ω \land B \subset A) \to \neg A \approx B$
7		ensymfib	$⊢ A \in Fin \to (A \approx B \leftrightarrow B \approx A)$
8	7	biimprd	$⊢ A \in Fin \to (B \approx A \to A \approx B)$
9	1 8	syl	$⊢ A \in ω \to (B \approx A \to A \approx B)$
10	9	adantr	$⊢ (A \in ω \land B \subset A) \to (B \approx A \to A \approx B)$
11	6 10	mtod	$⊢ (A \in ω \land B \subset A) \to \neg B \approx A$
12		brsdom	$⊢ B ≺ A \leftrightarrow (B ≼ A \land \neg B \approx A)$
13	5 11 12	sylanbrc	$⊢ (A \in ω \land B \subset A) \to B ≺ A$

Metamath Proof Explorer