Metamath Proof Explorer

Theorem phpreu

Description: Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Assertion phpreu ⊢A∈Fin∧A≈B→∀x∈A∃y∈Bx=C↔∀x∈A∃!y∈Bx=C

Proof

Step Hyp Ref Expression
1 eleq1 ⊢x=C→x∈A↔C∈A
2 1 biimpac ⊢x∈A∧x=C→C∈A
3 rabid ⊢y∈y∈B|C∈A↔y∈B∧C∈A
4 3 simplbi2com ⊢C∈A→y∈B→y∈y∈B|C∈A
5 2 4 syl ⊢x∈A∧x=C→y∈B→y∈y∈B|C∈A
6 5 impancom ⊢x∈A∧y∈B→x=C→y∈y∈B|C∈A
7 6 ancrd ⊢x∈A∧y∈B→x=C→y∈y∈B|C∈A∧x=C
8 7 expimpd ⊢x∈A→y∈B∧x=C→y∈y∈B|C∈A∧x=C
9 8 reximdv2 ⊢x∈A→∃y∈Bx=C→∃y∈y∈B|C∈Ax=C
10 9 ralimia ⊢∀x∈A∃y∈Bx=C→∀x∈A∃y∈y∈B|C∈Ax=C
11 3 simplbi ⊢y∈y∈B|C∈A→y∈B
12 6 pm4.71rd ⊢x∈A∧y∈B→x=C↔y∈y∈B|C∈A∧x=C
13 df-mpt ⊢y∈y∈B|C∈A⟼C=yx|y∈y∈B|C∈A∧x=C
14 13 breqi ⊢yy∈y∈B|C∈A⟼Cx↔yyx|y∈y∈B|C∈A∧x=Cx
15 df-br ⊢yyx|y∈y∈B|C∈A∧x=Cx↔yx∈yx|y∈y∈B|C∈A∧x=C
16 opabidw ⊢yx∈yx|y∈y∈B|C∈A∧x=C↔y∈y∈B|C∈A∧x=C
17 14 15 16 3bitri ⊢yy∈y∈B|C∈A⟼Cx↔y∈y∈B|C∈A∧x=C
18 12 17 bitr4di ⊢x∈A∧y∈B→x=C↔yy∈y∈B|C∈A⟼Cx
19 11 18 sylan2 ⊢x∈A∧y∈y∈B|C∈A→x=C↔yy∈y∈B|C∈A⟼Cx
20 19 rexbidva ⊢x∈A→∃y∈y∈B|C∈Ax=C↔∃y∈y∈B|C∈Ayy∈y∈B|C∈A⟼Cx
21 20 ralbiia ⊢∀x∈A∃y∈y∈B|C∈Ax=C↔∀x∈A∃y∈y∈B|C∈Ayy∈y∈B|C∈A⟼Cx
22 breq2 ⊢a=x→by∈y∈B|C∈A⟼Ca↔by∈y∈B|C∈A⟼Cx
23 22 rexbidv ⊢a=x→∃b∈y∈B|C∈Aby∈y∈B|C∈A⟼Ca↔∃b∈y∈B|C∈Aby∈y∈B|C∈A⟼Cx
24 nfcv ⊢Ⅎ_by∈B|C∈A
25 nfrab1 ⊢Ⅎ_yy∈B|C∈A
26 nfcv ⊢Ⅎ_yb
27 nfmpt1 ⊢Ⅎ_yy∈y∈B|C∈A⟼C
28 nfcv ⊢Ⅎ_yx
29 26 27 28 nfbr ⊢Ⅎyby∈y∈B|C∈A⟼Cx
30 nfv ⊢Ⅎbyy∈y∈B|C∈A⟼Cx
31 breq1 ⊢b=y→by∈y∈B|C∈A⟼Cx↔yy∈y∈B|C∈A⟼Cx
32 24 25 29 30 31 cbvrexfw ⊢∃b∈y∈B|C∈Aby∈y∈B|C∈A⟼Cx↔∃y∈y∈B|C∈Ayy∈y∈B|C∈A⟼Cx
33 23 32 bitrdi ⊢a=x→∃b∈y∈B|C∈Aby∈y∈B|C∈A⟼Ca↔∃y∈y∈B|C∈Ayy∈y∈B|C∈A⟼Cx
34 33 cbvralvw ⊢∀a∈A∃b∈y∈B|C∈Aby∈y∈B|C∈A⟼Ca↔∀x∈A∃y∈y∈B|C∈Ayy∈y∈B|C∈A⟼Cx
35 21 34 bitr4i ⊢∀x∈A∃y∈y∈B|C∈Ax=C↔∀a∈A∃b∈y∈B|C∈Aby∈y∈B|C∈A⟼Ca
36 10 35 sylib ⊢∀x∈A∃y∈Bx=C→∀a∈A∃b∈y∈B|C∈Aby∈y∈B|C∈A⟼Ca
37 nfv ⊢Ⅎby∈y∈B|C∈A∧x=C
38 25 nfcri ⊢Ⅎyb∈y∈B|C∈A
39 nfcsb1v ⊢Ⅎ_y⦋b/y⦌C
40 39 nfeq2 ⊢Ⅎyx=⦋b/y⦌C
41 38 40 nfan ⊢Ⅎyb∈y∈B|C∈A∧x=⦋b/y⦌C
42 eleq1 ⊢y=b→y∈y∈B|C∈A↔b∈y∈B|C∈A
43 csbeq1a ⊢y=b→C=⦋b/y⦌C
44 43 eqeq2d ⊢y=b→x=C↔x=⦋b/y⦌C
45 42 44 anbi12d ⊢y=b→y∈y∈B|C∈A∧x=C↔b∈y∈B|C∈A∧x=⦋b/y⦌C
46 37 41 45 cbvopab1 ⊢yx|y∈y∈B|C∈A∧x=C=bx|b∈y∈B|C∈A∧x=⦋b/y⦌C
47 df-mpt ⊢b∈y∈B|C∈A⟼⦋b/y⦌C=bx|b∈y∈B|C∈A∧x=⦋b/y⦌C
48 46 13 47 3eqtr4i ⊢y∈y∈B|C∈A⟼C=b∈y∈B|C∈A⟼⦋b/y⦌C
49 nfcv ⊢Ⅎ_yB
50 39 nfel1 ⊢Ⅎy⦋b/y⦌C∈A
51 43 eleq1d ⊢y=b→C∈A↔⦋b/y⦌C∈A
52 26 49 50 51 elrabf ⊢b∈y∈B|C∈A↔b∈B∧⦋b/y⦌C∈A
53 52 simprbi ⊢b∈y∈B|C∈A→⦋b/y⦌C∈A
54 48 53 fmpti ⊢y∈y∈B|C∈A⟼C:y∈B|C∈A⟶A
55 36 54 jctil ⊢∀x∈A∃y∈Bx=C→y∈y∈B|C∈A⟼C:y∈B|C∈A⟶A∧∀a∈A∃b∈y∈B|C∈Aby∈y∈B|C∈A⟼Ca
56 dffo4 ⊢y∈y∈B|C∈A⟼C:y∈B|C∈A⟶ontoA↔y∈y∈B|C∈A⟼C:y∈B|C∈A⟶A∧∀a∈A∃b∈y∈B|C∈Aby∈y∈B|C∈A⟼Ca
57 55 56 sylibr ⊢∀x∈A∃y∈Bx=C→y∈y∈B|C∈A⟼C:y∈B|C∈A⟶ontoA
58 57 adantl ⊢A∈Fin∧A≈B∧∀x∈A∃y∈Bx=C→y∈y∈B|C∈A⟼C:y∈B|C∈A⟶ontoA
59 relen ⊢Rel⁡≈
60 59 brrelex2i ⊢A≈B→B∈V
61 ssrab2 ⊢y∈B|C∈A⊆B
62 ssdomg ⊢B∈V→y∈B|C∈A⊆B→y∈B|C∈A≼B
63 60 61 62 mpisyl ⊢A≈B→y∈B|C∈A≼B
64 ensym ⊢A≈B→B≈A
65 domentr ⊢y∈B|C∈A≼B∧B≈A→y∈B|C∈A≼A
66 63 64 65 syl2anc ⊢A≈B→y∈B|C∈A≼A
67 66 ad2antlr ⊢A∈Fin∧A≈B∧∀x∈A∃y∈Bx=C→y∈B|C∈A≼A
68 enfi ⊢A≈B→A∈Fin↔B∈Fin
69 68 biimpac ⊢A∈Fin∧A≈B→B∈Fin
70 rabfi ⊢B∈Fin→y∈B|C∈A∈Fin
71 69 70 syl ⊢A∈Fin∧A≈B→y∈B|C∈A∈Fin
72 fodomfi ⊢y∈B|C∈A∈Fin∧y∈y∈B|C∈A⟼C:y∈B|C∈A⟶ontoA→A≼y∈B|C∈A
73 71 57 72 syl2an ⊢A∈Fin∧A≈B∧∀x∈A∃y∈Bx=C→A≼y∈B|C∈A
74 sbth ⊢y∈B|C∈A≼A∧A≼y∈B|C∈A→y∈B|C∈A≈A
75 67 73 74 syl2anc ⊢A∈Fin∧A≈B∧∀x∈A∃y∈Bx=C→y∈B|C∈A≈A
76 simpll ⊢A∈Fin∧A≈B∧∀x∈A∃y∈Bx=C→A∈Fin
77 fofinf1o ⊢y∈y∈B|C∈A⟼C:y∈B|C∈A⟶ontoA∧y∈B|C∈A≈A∧A∈Fin→y∈y∈B|C∈A⟼C:y∈B|C∈A⟶1-1 ontoA
78 58 75 76 77 syl3anc ⊢A∈Fin∧A≈B∧∀x∈A∃y∈Bx=C→y∈y∈B|C∈A⟼C:y∈B|C∈A⟶1-1 ontoA
79 f1of1 ⊢y∈y∈B|C∈A⟼C:y∈B|C∈A⟶1-1 ontoA→y∈y∈B|C∈A⟼C:y∈B|C∈A⟶1-1A
80 78 79 syl ⊢A∈Fin∧A≈B∧∀x∈A∃y∈Bx=C→y∈y∈B|C∈A⟼C:y∈B|C∈A⟶1-1A
81 dff12 ⊢y∈y∈B|C∈A⟼C:y∈B|C∈A⟶1-1A↔y∈y∈B|C∈A⟼C:y∈B|C∈A⟶A∧∀a∃*bby∈y∈B|C∈A⟼Ca
82 81 simprbi ⊢y∈y∈B|C∈A⟼C:y∈B|C∈A⟶1-1A→∀a∃*bby∈y∈B|C∈A⟼Ca
83 22 mobidv ⊢a=x→∃*bby∈y∈B|C∈A⟼Ca↔∃*bby∈y∈B|C∈A⟼Cx
84 29 30 31 cbvmow ⊢∃*bby∈y∈B|C∈A⟼Cx↔∃*yyy∈y∈B|C∈A⟼Cx
85 83 84 bitrdi ⊢a=x→∃*bby∈y∈B|C∈A⟼Ca↔∃*yyy∈y∈B|C∈A⟼Cx
86 85 cbvalvw ⊢∀a∃*bby∈y∈B|C∈A⟼Ca↔∀x∃*yyy∈y∈B|C∈A⟼Cx
87 82 86 sylib ⊢y∈y∈B|C∈A⟼C:y∈B|C∈A⟶1-1A→∀x∃*yyy∈y∈B|C∈A⟼Cx
88 mormo ⊢∃*yyy∈y∈B|C∈A⟼Cx→∃*y∈Byy∈y∈B|C∈A⟼Cx
89 88 alimi ⊢∀x∃*yyy∈y∈B|C∈A⟼Cx→∀x∃*y∈Byy∈y∈B|C∈A⟼Cx
90 alral ⊢∀x∃*y∈Byy∈y∈B|C∈A⟼Cx→∀x∈A∃*y∈Byy∈y∈B|C∈A⟼Cx
91 80 87 89 90 4syl ⊢A∈Fin∧A≈B∧∀x∈A∃y∈Bx=C→∀x∈A∃*y∈Byy∈y∈B|C∈A⟼Cx
92 18 rmobidva ⊢x∈A→∃*y∈Bx=C↔∃*y∈Byy∈y∈B|C∈A⟼Cx
93 92 ralbiia ⊢∀x∈A∃*y∈Bx=C↔∀x∈A∃*y∈Byy∈y∈B|C∈A⟼Cx
94 91 93 sylibr ⊢A∈Fin∧A≈B∧∀x∈A∃y∈Bx=C→∀x∈A∃*y∈Bx=C
95 94 ex ⊢A∈Fin∧A≈B→∀x∈A∃y∈Bx=C→∀x∈A∃*y∈Bx=C
96 95 pm4.71d ⊢A∈Fin∧A≈B→∀x∈A∃y∈Bx=C↔∀x∈A∃y∈Bx=C∧∀x∈A∃*y∈Bx=C
97 reu5 ⊢∃!y∈Bx=C↔∃y∈Bx=C∧∃*y∈Bx=C
98 97 ralbii ⊢∀x∈A∃!y∈Bx=C↔∀x∈A∃y∈Bx=C∧∃*y∈Bx=C
99 r19.26 ⊢∀x∈A∃y∈Bx=C∧∃*y∈Bx=C↔∀x∈A∃y∈Bx=C∧∀x∈A∃*y∈Bx=C
100 98 99 bitri ⊢∀x∈A∃!y∈Bx=C↔∀x∈A∃y∈Bx=C∧∀x∈A∃*y∈Bx=C
101 96 100 bitr4di ⊢A∈Fin∧A≈B→∀x∈A∃y∈Bx=C↔∀x∈A∃!y∈Bx=C