# Metamath Proof Explorer

## 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 ℕ$
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}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{D}={y}\right\}\approx ℕ$

### Proof

Step Hyp Ref Expression
1 fiphp3d.a ${⊢}{\phi }\to {A}\approx ℕ$
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 ${⊢}¬\mathrm{\omega }\in \mathrm{Fin}$
5 risset ${⊢}{D}\in {B}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}={D}$
6 eqcom ${⊢}{y}={D}↔{D}={y}$
7 6 rexbii ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}={D}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={y}$
8 5 7 bitri ${⊢}{D}\in {B}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={y}$
9 3 8 sylib ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={y}$
10 9 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={y}$
11 rabid2 ${⊢}{A}=\left\{{x}\in {A}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={y}\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={y}$
12 10 11 sylibr ${⊢}{\phi }\to {A}=\left\{{x}\in {A}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={y}\right\}$
13 iunrab ${⊢}\bigcup _{{y}\in {B}}\left\{{x}\in {A}|{D}={y}\right\}=\left\{{x}\in {A}|\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={y}\right\}$
14 12 13 syl6reqr ${⊢}{\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}↔{A}\in \mathrm{Fin}\right)$
16 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
17 entr ${⊢}\left({A}\approx ℕ\wedge ℕ\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}↔\mathrm{\omega }\in \mathrm{Fin}\right)$
20 18 19 syl ${⊢}{\phi }\to \left({A}\in \mathrm{Fin}↔\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}↔\mathrm{\omega }\in \mathrm{Fin}\right)$
22 4 21 mtbiri ${⊢}{\phi }\to ¬\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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 ¬\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}$
26 rexnal ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}¬\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}↔¬\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}$
27 25 26 sylibr ${⊢}{\phi }\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}¬\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}$
28 18 16 jctir ${⊢}{\phi }\to \left({A}\approx \mathrm{\omega }\wedge ℕ\approx \mathrm{\omega }\right)$
29 ssrab2 ${⊢}\left\{{x}\in {A}|{D}={y}\right\}\subseteq {A}$
30 29 jctl ${⊢}¬\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}\to \left(\left\{{x}\in {A}|{D}={y}\right\}\subseteq {A}\wedge ¬\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}\right)$
31 ctbnfien ${⊢}\left(\left({A}\approx \mathrm{\omega }\wedge ℕ\approx \mathrm{\omega }\right)\wedge \left(\left\{{x}\in {A}|{D}={y}\right\}\subseteq {A}\wedge ¬\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}\right)\right)\to \left\{{x}\in {A}|{D}={y}\right\}\approx ℕ$
32 28 30 31 syl2an ${⊢}\left({\phi }\wedge ¬\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}\right)\to \left\{{x}\in {A}|{D}={y}\right\}\approx ℕ$
33 32 ex ${⊢}{\phi }\to \left(¬\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}\to \left\{{x}\in {A}|{D}={y}\right\}\approx ℕ\right)$
34 33 reximdv ${⊢}{\phi }\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}¬\left\{{x}\in {A}|{D}={y}\right\}\in \mathrm{Fin}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{D}={y}\right\}\approx ℕ\right)$
35 27 34 mpd ${⊢}{\phi }\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{D}={y}\right\}\approx ℕ$