Theorem fiphp3d

Description: Infinite pigeonhole principle for partitioning an infinite set between finitely many buckets. (Contributed by Stefan O'Rear, 18-Oct-2014)

	Ref	Expression
Hypotheses	fiphp3d.a	$$⊢\phi \to A\approx \mathbb{N}$$
	fiphp3d.b	$$⊢\phi \to B\in \mathrm{Fin}$$
	fiphp3d.c	$$⊢\left(\phi \wedge x\in A\right)\to D\in B$$
Assertion	fiphp3d	$$⊢\phi \to \exists y\in B\left\{x\in A|D=y\right\}\approx \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		fiphp3d.a	$$⊢\phi \to A\approx \mathbb{N}$$
2		fiphp3d.b	$$⊢\phi \to B\in \mathrm{Fin}$$
3		fiphp3d.c	$$⊢\left(\phi \wedge x\in A\right)\to D\in B$$
4		ominf	$$⊢\neg \mathrm{\omega }\in \mathrm{Fin}$$
5		iunrab	$$⊢\bigcup _{y\in B}\left\{x\in A|D=y\right\}=\left\{x\in A|\exists y\in BD=y\right\}$$
6		risset	$$⊢D\in B\leftrightarrow \exists y\in By=D$$
7		eqcom	$$⊢y=D\leftrightarrow D=y$$
8	7	rexbii	$$⊢\exists y\in By=D\leftrightarrow \exists y\in BD=y$$
9	6 8	bitri	$$⊢D\in B\leftrightarrow \exists y\in BD=y$$
10	3 9	sylib	$$⊢\left(\phi \wedge x\in A\right)\to \exists y\in BD=y$$
11	10	ralrimiva	$$⊢\phi \to \forall x\in A\exists y\in BD=y$$
12		rabid2	$$⊢A=\left\{x\in A|\exists y\in BD=y\right\}\leftrightarrow \forall x\in A\exists y\in BD=y$$
13	11 12	sylibr	$$⊢\phi \to A=\left\{x\in A|\exists y\in BD=y\right\}$$
14	5 13	eqtr4id	$$⊢\phi \to \bigcup _{y\in B}\left\{x\in A|D=y\right\}=A$$
15	14	eleq1d	$$⊢\phi \to \left(\bigcup _{y\in B}\left\{x\in A|D=y\right\}\in \mathrm{Fin}\leftrightarrow A\in \mathrm{Fin}\right)$$
16		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
17		entr	$$⊢\left(A\approx \mathbb{N}\wedge \mathbb{N}\approx \mathrm{\omega }\right)\to A\approx \mathrm{\omega }$$
18	1 16 17	sylancl	$$⊢\phi \to A\approx \mathrm{\omega }$$
19		enfi	$$⊢A\approx \mathrm{\omega }\to \left(A\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\in \mathrm{Fin}\right)$$
20	18 19	syl	$$⊢\phi \to \left(A\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\in \mathrm{Fin}\right)$$
21	15 20	bitrd	$$⊢\phi \to \left(\bigcup _{y\in B}\left\{x\in A|D=y\right\}\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\in \mathrm{Fin}\right)$$
22	4 21	mtbiri	$$⊢\phi \to \neg \bigcup _{y\in B}\left\{x\in A|D=y\right\}\in \mathrm{Fin}$$
23		iunfi	$$⊢\left(B\in \mathrm{Fin}\wedge \forall y\in B\left\{x\in A|D=y\right\}\in \mathrm{Fin}\right)\to \bigcup _{y\in B}\left\{x\in A|D=y\right\}\in \mathrm{Fin}$$
24	2 23	sylan	$$⊢\left(\phi \wedge \forall y\in B\left\{x\in A|D=y\right\}\in \mathrm{Fin}\right)\to \bigcup _{y\in B}\left\{x\in A|D=y\right\}\in \mathrm{Fin}$$
25	22 24	mtand	$$⊢\phi \to \neg \forall y\in B\left\{x\in A|D=y\right\}\in \mathrm{Fin}$$
26		rexnal	$$⊢\exists y\in B\neg \left\{x\in A|D=y\right\}\in \mathrm{Fin}\leftrightarrow \neg \forall y\in B\left\{x\in A|D=y\right\}\in \mathrm{Fin}$$
27	25 26	sylibr	$$⊢\phi \to \exists y\in B\neg \left\{x\in A|D=y\right\}\in \mathrm{Fin}$$
28	18 16	jctir	$$⊢\phi \to \left(A\approx \mathrm{\omega }\wedge \mathbb{N}\approx \mathrm{\omega }\right)$$
29		ssrab2	$$⊢\left\{x\in A|D=y\right\}\subseteq A$$
30	29	jctl	$$⊢\neg \left\{x\in A|D=y\right\}\in \mathrm{Fin}\to \left(\left\{x\in A|D=y\right\}\subseteq A\wedge \neg \left\{x\in A|D=y\right\}\in \mathrm{Fin}\right)$$
31		ctbnfien	$$⊢\left(\left(A\approx \mathrm{\omega }\wedge \mathbb{N}\approx \mathrm{\omega }\right)\wedge \left(\left\{x\in A|D=y\right\}\subseteq A\wedge \neg \left\{x\in A|D=y\right\}\in \mathrm{Fin}\right)\right)\to \left\{x\in A|D=y\right\}\approx \mathbb{N}$$
32	28 30 31	syl2an	$$⊢\left(\phi \wedge \neg \left\{x\in A|D=y\right\}\in \mathrm{Fin}\right)\to \left\{x\in A|D=y\right\}\approx \mathbb{N}$$
33	32	ex	$$⊢\phi \to \left(\neg \left\{x\in A|D=y\right\}\in \mathrm{Fin}\to \left\{x\in A|D=y\right\}\approx \mathbb{N}\right)$$
34	33	reximdv	$$⊢\phi \to \left(\exists y\in B\neg \left\{x\in A|D=y\right\}\in \mathrm{Fin}\to \exists y\in B\left\{x\in A|D=y\right\}\approx \mathbb{N}\right)$$
35	27 34	mpd	$$⊢\phi \to \exists y\in B\left\{x\in A|D=y\right\}\approx \mathbb{N}$$