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 φ A
fiphp3d.b φ B Fin
fiphp3d.c φ x A D B
Assertion fiphp3d φ y B x A | D = y

Proof

Step Hyp Ref Expression
1 fiphp3d.a φ A
2 fiphp3d.b φ B Fin
3 fiphp3d.c φ x A D B
4 ominf ¬ ω Fin
5 risset D B y B y = D
6 eqcom y = D D = y
7 6 rexbii y B y = D y B D = y
8 5 7 bitri D B y B D = y
9 3 8 sylib φ x A y B D = y
10 9 ralrimiva φ x A y B D = y
11 rabid2 A = x A | y B D = y x A y B D = y
12 10 11 sylibr φ A = x A | y B D = y
13 iunrab y B x A | D = y = x A | y B D = y
14 12 13 syl6reqr φ y B x A | D = y = A
15 14 eleq1d φ y B x A | D = y Fin A Fin
16 nnenom ω
17 entr A ω A ω
18 1 16 17 sylancl φ A ω
19 enfi A ω A Fin ω Fin
20 18 19 syl φ A Fin ω Fin
21 15 20 bitrd φ y B x A | D = y Fin ω Fin
22 4 21 mtbiri φ ¬ y B x A | D = y Fin
23 iunfi B Fin y B x A | D = y Fin y B x A | D = y Fin
24 2 23 sylan φ y B x A | D = y Fin y B x A | D = y Fin
25 22 24 mtand φ ¬ y B x A | D = y Fin
26 rexnal y B ¬ x A | D = y Fin ¬ y B x A | D = y Fin
27 25 26 sylibr φ y B ¬ x A | D = y Fin
28 18 16 jctir φ A ω ω
29 ssrab2 x A | D = y A
30 29 jctl ¬ x A | D = y Fin x A | D = y A ¬ x A | D = y Fin
31 ctbnfien A ω ω x A | D = y A ¬ x A | D = y Fin x A | D = y
32 28 30 31 syl2an φ ¬ x A | D = y Fin x A | D = y
33 32 ex φ ¬ x A | D = y Fin x A | D = y
34 33 reximdv φ y B ¬ x A | D = y Fin y B x A | D = y
35 27 34 mpd φ y B x A | D = y