Theorem 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	$$⊢\left(A\in \mathrm{\omega }\wedge B\subset A\right)\to B\prec A$$

Proof

Step	Hyp	Ref	Expression
1		nnfi	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$
2		pssss	$$⊢B\subset A\to B\subseteq A$$
3		ssdomfi	$$⊢A\in \mathrm{Fin}\to \left(B\subseteq A\to B\preccurlyeq A\right)$$
4	3	imp	$$⊢\left(A\in \mathrm{Fin}\wedge B\subseteq A\right)\to B\preccurlyeq A$$
5	1 2 4	syl2an	$$⊢\left(A\in \mathrm{\omega }\wedge B\subset A\right)\to B\preccurlyeq A$$
6		php	$$⊢\left(A\in \mathrm{\omega }\wedge B\subset A\right)\to \neg A\approx B$$
7		ensymfib	$$⊢A\in \mathrm{Fin}\to \left(A\approx B\leftrightarrow B\approx A\right)$$
8	7	biimprd	$$⊢A\in \mathrm{Fin}\to \left(B\approx A\to A\approx B\right)$$
9	1 8	syl	$$⊢A\in \mathrm{\omega }\to \left(B\approx A\to A\approx B\right)$$
10	9	adantr	$$⊢\left(A\in \mathrm{\omega }\wedge B\subset A\right)\to \left(B\approx A\to A\approx B\right)$$
11	6 10	mtod	$$⊢\left(A\in \mathrm{\omega }\wedge B\subset A\right)\to \neg B\approx A$$
12		brsdom	$$⊢B\prec A\leftrightarrow \left(B\preccurlyeq A\wedge \neg B\approx A\right)$$
13	5 11 12	sylanbrc	$$⊢\left(A\in \mathrm{\omega }\wedge B\subset A\right)\to B\prec A$$