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 
|- ( ph -> A ~~ NN )
fiphp3d.b 
|- ( ph -> B e. Fin )
fiphp3d.c 
|- ( ( ph /\ x e. A ) -> D e. B )
Assertion fiphp3d 
|- ( ph -> E. y e. B { x e. A | D = y } ~~ NN )

Proof

Step Hyp Ref Expression
1 fiphp3d.a 
 |-  ( ph -> A ~~ NN )
2 fiphp3d.b 
 |-  ( ph -> B e. Fin )
3 fiphp3d.c 
 |-  ( ( ph /\ x e. A ) -> D e. B )
4 ominf 
 |-  -. _om e. Fin
5 iunrab 
 |-  U_ y e. B { x e. A | D = y } = { x e. A | E. y e. B D = y }
6 risset 
 |-  ( D e. B <-> E. y e. B y = D )
7 eqcom 
 |-  ( y = D <-> D = y )
8 7 rexbii 
 |-  ( E. y e. B y = D <-> E. y e. B D = y )
9 6 8 bitri 
 |-  ( D e. B <-> E. y e. B D = y )
10 3 9 sylib 
 |-  ( ( ph /\ x e. A ) -> E. y e. B D = y )
11 10 ralrimiva 
 |-  ( ph -> A. x e. A E. y e. B D = y )
12 rabid2 
 |-  ( A = { x e. A | E. y e. B D = y } <-> A. x e. A E. y e. B D = y )
13 11 12 sylibr 
 |-  ( ph -> A = { x e. A | E. y e. B D = y } )
14 5 13 eqtr4id 
 |-  ( ph -> U_ y e. B { x e. A | D = y } = A )
15 14 eleq1d 
 |-  ( ph -> ( U_ y e. B { x e. A | D = y } e. Fin <-> A e. Fin ) )
16 nnenom 
 |-  NN ~~ _om
17 entr 
 |-  ( ( A ~~ NN /\ NN ~~ _om ) -> A ~~ _om )
18 1 16 17 sylancl 
 |-  ( ph -> A ~~ _om )
19 enfi 
 |-  ( A ~~ _om -> ( A e. Fin <-> _om e. Fin ) )
20 18 19 syl 
 |-  ( ph -> ( A e. Fin <-> _om e. Fin ) )
21 15 20 bitrd 
 |-  ( ph -> ( U_ y e. B { x e. A | D = y } e. Fin <-> _om e. Fin ) )
22 4 21 mtbiri 
 |-  ( ph -> -. U_ y e. B { x e. A | D = y } e. Fin )
23 iunfi 
 |-  ( ( B e. Fin /\ A. y e. B { x e. A | D = y } e. Fin ) -> U_ y e. B { x e. A | D = y } e. Fin )
24 2 23 sylan 
 |-  ( ( ph /\ A. y e. B { x e. A | D = y } e. Fin ) -> U_ y e. B { x e. A | D = y } e. Fin )
25 22 24 mtand 
 |-  ( ph -> -. A. y e. B { x e. A | D = y } e. Fin )
26 rexnal 
 |-  ( E. y e. B -. { x e. A | D = y } e. Fin <-> -. A. y e. B { x e. A | D = y } e. Fin )
27 25 26 sylibr 
 |-  ( ph -> E. y e. B -. { x e. A | D = y } e. Fin )
28 18 16 jctir 
 |-  ( ph -> ( A ~~ _om /\ NN ~~ _om ) )
29 ssrab2 
 |-  { x e. A | D = y } C_ A
30 29 jctl 
 |-  ( -. { x e. A | D = y } e. Fin -> ( { x e. A | D = y } C_ A /\ -. { x e. A | D = y } e. Fin ) )
31 ctbnfien 
 |-  ( ( ( A ~~ _om /\ NN ~~ _om ) /\ ( { x e. A | D = y } C_ A /\ -. { x e. A | D = y } e. Fin ) ) -> { x e. A | D = y } ~~ NN )
32 28 30 31 syl2an 
 |-  ( ( ph /\ -. { x e. A | D = y } e. Fin ) -> { x e. A | D = y } ~~ NN )
33 32 ex 
 |-  ( ph -> ( -. { x e. A | D = y } e. Fin -> { x e. A | D = y } ~~ NN ) )
34 33 reximdv 
 |-  ( ph -> ( E. y e. B -. { x e. A | D = y } e. Fin -> E. y e. B { x e. A | D = y } ~~ NN ) )
35 27 34 mpd 
 |-  ( ph -> E. y e. B { x e. A | D = y } ~~ NN )