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 ∈ B x = C ↔ ∀ x ∈ A ∃! y ∈ B x = 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 ∈ B x = C → ∃ y ∈ y ∈ B | C ∈ A x = C
10 9 ralimia ⊢ ∀ x ∈ A ∃ y ∈ B x = C → ∀ x ∈ A ∃ y ∈ y ∈ B | C ∈ A x = 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 = y x | y ∈ y ∈ B | C ∈ A ∧ x = C
14 13 breqi ⊢ y y ∈ y ∈ B | C ∈ A ⟼ C x ↔ y y x | y ∈ y ∈ B | C ∈ A ∧ x = C x
15 df-br ⊢ y y x | y ∈ y ∈ B | C ∈ A ∧ x = C x ↔ y x ∈ y x | y ∈ y ∈ B | C ∈ A ∧ x = C
16 opabidw ⊢ y x ∈ y x | y ∈ y ∈ B | C ∈ A ∧ x = C ↔ y ∈ y ∈ B | C ∈ A ∧ x = C
17 14 15 16 3bitri ⊢ y y ∈ y ∈ B | C ∈ A ⟼ C x ↔ y ∈ y ∈ B | C ∈ A ∧ x = C
18 12 17 bitr4di ⊢ x ∈ A ∧ y ∈ B → x = C ↔ y y ∈ y ∈ B | C ∈ A ⟼ C x
19 11 18 sylan2 ⊢ x ∈ A ∧ y ∈ y ∈ B | C ∈ A → x = C ↔ y y ∈ y ∈ B | C ∈ A ⟼ C x
20 19 rexbidva ⊢ x ∈ A → ∃ y ∈ y ∈ B | C ∈ A x = C ↔ ∃ y ∈ y ∈ B | C ∈ A y y ∈ y ∈ B | C ∈ A ⟼ C x
21 20 ralbiia ⊢ ∀ x ∈ A ∃ y ∈ y ∈ B | C ∈ A x = C ↔ ∀ x ∈ A ∃ y ∈ y ∈ B | C ∈ A y y ∈ y ∈ B | C ∈ A ⟼ C x
22 breq2 ⊢ a = x → b y ∈ y ∈ B | C ∈ A ⟼ C a ↔ b y ∈ y ∈ B | C ∈ A ⟼ C x
23 22 rexbidv ⊢ a = x → ∃ b ∈ y ∈ B | C ∈ A b y ∈ y ∈ B | C ∈ A ⟼ C a ↔ ∃ b ∈ y ∈ B | C ∈ A b y ∈ y ∈ B | C ∈ A ⟼ C x
24 nfcv ⊢ Ⅎ _ b y ∈ B | C ∈ A
25 nfrab1 ⊢ Ⅎ _ y y ∈ B | C ∈ A
26 nfcv ⊢ Ⅎ _ y b
27 nfmpt1 ⊢ Ⅎ _ y y ∈ y ∈ B | C ∈ A ⟼ C
28 nfcv ⊢ Ⅎ _ y x
29 26 27 28 nfbr ⊢ Ⅎ y b y ∈ y ∈ B | C ∈ A ⟼ C x
30 nfv ⊢ Ⅎ b y y ∈ y ∈ B | C ∈ A ⟼ C x
31 breq1 ⊢ b = y → b y ∈ y ∈ B | C ∈ A ⟼ C x ↔ y y ∈ y ∈ B | C ∈ A ⟼ C x
32 24 25 29 30 31 cbvrexfw ⊢ ∃ b ∈ y ∈ B | C ∈ A b y ∈ y ∈ B | C ∈ A ⟼ C x ↔ ∃ y ∈ y ∈ B | C ∈ A y y ∈ y ∈ B | C ∈ A ⟼ C x
33 23 32 bitrdi ⊢ a = x → ∃ b ∈ y ∈ B | C ∈ A b y ∈ y ∈ B | C ∈ A ⟼ C a ↔ ∃ y ∈ y ∈ B | C ∈ A y y ∈ y ∈ B | C ∈ A ⟼ C x
34 33 cbvralvw ⊢ ∀ a ∈ A ∃ b ∈ y ∈ B | C ∈ A b y ∈ y ∈ B | C ∈ A ⟼ C a ↔ ∀ x ∈ A ∃ y ∈ y ∈ B | C ∈ A y y ∈ y ∈ B | C ∈ A ⟼ C x
35 21 34 bitr4i ⊢ ∀ x ∈ A ∃ y ∈ y ∈ B | C ∈ A x = C ↔ ∀ a ∈ A ∃ b ∈ y ∈ B | C ∈ A b y ∈ y ∈ B | C ∈ A ⟼ C a
36 10 35 sylib ⊢ ∀ x ∈ A ∃ y ∈ B x = C → ∀ a ∈ A ∃ b ∈ y ∈ B | C ∈ A b y ∈ y ∈ B | C ∈ A ⟼ C a
37 nfv ⊢ Ⅎ b y ∈ y ∈ B | C ∈ A ∧ x = C
38 25 nfcri ⊢ Ⅎ y b ∈ y ∈ B | C ∈ A
39 nfcsb1v ⊢ Ⅎ _ y ⦋ b / y⦌ C
40 39 nfeq2 ⊢ Ⅎ y x = ⦋ b / y⦌ C
41 38 40 nfan ⊢ Ⅎ y b ∈ 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 ⊢ y x | y ∈ y ∈ B | C ∈ A ∧ x = C = b x | b ∈ y ∈ B | C ∈ A ∧ x = ⦋ b / y⦌ C
47 df-mpt ⊢ b ∈ y ∈ B | C ∈ A ⟼ ⦋ b / y⦌ C = b x | 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 ⊢ Ⅎ _ y B
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 ∈ B x = C → y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ A ∧ ∀ a ∈ A ∃ b ∈ y ∈ B | C ∈ A b y ∈ y ∈ B | C ∈ A ⟼ C a
56 dffo4 ⊢ y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ onto A ↔ y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ A ∧ ∀ a ∈ A ∃ b ∈ y ∈ B | C ∈ A b y ∈ y ∈ B | C ∈ A ⟼ C a
57 55 56 sylibr ⊢ ∀ x ∈ A ∃ y ∈ B x = C → y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ onto A
58 57 adantl ⊢ A ∈ Fin ∧ A ≈ B ∧ ∀ x ∈ A ∃ y ∈ B x = C → y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ onto A
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 ∈ B x = 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 ⟶ onto A → A ≼ y ∈ B | C ∈ A
73 71 57 72 syl2an ⊢ A ∈ Fin ∧ A ≈ B ∧ ∀ x ∈ A ∃ y ∈ B x = 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 ∈ B x = C → y ∈ B | C ∈ A ≈ A
76 simpll ⊢ A ∈ Fin ∧ A ≈ B ∧ ∀ x ∈ A ∃ y ∈ B x = C → A ∈ Fin
77 fofinf1o ⊢ y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ onto A ∧ y ∈ B | C ∈ A ≈ A ∧ A ∈ Fin → y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ 1-1 onto A
78 58 75 76 77 syl3anc ⊢ A ∈ Fin ∧ A ≈ B ∧ ∀ x ∈ A ∃ y ∈ B x = C → y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ 1-1 onto A
79 f1of1 ⊢ y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ 1-1 onto A → y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ 1-1 A
80 78 79 syl ⊢ A ∈ Fin ∧ A ≈ B ∧ ∀ x ∈ A ∃ y ∈ B x = C → y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ 1-1 A
81 dff12 ⊢ y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ 1-1 A ↔ y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ A ∧ ∀ a ∃* b b y ∈ y ∈ B | C ∈ A ⟼ C a
82 81 simprbi ⊢ y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ 1-1 A → ∀ a ∃* b b y ∈ y ∈ B | C ∈ A ⟼ C a
83 22 mobidv ⊢ a = x → ∃* b b y ∈ y ∈ B | C ∈ A ⟼ C a ↔ ∃* b b y ∈ y ∈ B | C ∈ A ⟼ C x
84 29 30 31 cbvmow ⊢ ∃* b b y ∈ y ∈ B | C ∈ A ⟼ C x ↔ ∃* y y y ∈ y ∈ B | C ∈ A ⟼ C x
85 83 84 bitrdi ⊢ a = x → ∃* b b y ∈ y ∈ B | C ∈ A ⟼ C a ↔ ∃* y y y ∈ y ∈ B | C ∈ A ⟼ C x
86 85 cbvalvw ⊢ ∀ a ∃* b b y ∈ y ∈ B | C ∈ A ⟼ C a ↔ ∀ x ∃* y y y ∈ y ∈ B | C ∈ A ⟼ C x
87 82 86 sylib ⊢ y ∈ y ∈ B | C ∈ A ⟼ C : y ∈ B | C ∈ A ⟶ 1-1 A → ∀ x ∃* y y y ∈ y ∈ B | C ∈ A ⟼ C x
88 mormo ⊢ ∃* y y y ∈ y ∈ B | C ∈ A ⟼ C x → ∃* y ∈ B y y ∈ y ∈ B | C ∈ A ⟼ C x
89 88 alimi ⊢ ∀ x ∃* y y y ∈ y ∈ B | C ∈ A ⟼ C x → ∀ x ∃* y ∈ B y y ∈ y ∈ B | C ∈ A ⟼ C x
90 alral ⊢ ∀ x ∃* y ∈ B y y ∈ y ∈ B | C ∈ A ⟼ C x → ∀ x ∈ A ∃* y ∈ B y y ∈ y ∈ B | C ∈ A ⟼ C x
91 80 87 89 90 4syl ⊢ A ∈ Fin ∧ A ≈ B ∧ ∀ x ∈ A ∃ y ∈ B x = C → ∀ x ∈ A ∃* y ∈ B y y ∈ y ∈ B | C ∈ A ⟼ C x
92 18 rmobidva ⊢ x ∈ A → ∃* y ∈ B x = C ↔ ∃* y ∈ B y y ∈ y ∈ B | C ∈ A ⟼ C x
93 92 ralbiia ⊢ ∀ x ∈ A ∃* y ∈ B x = C ↔ ∀ x ∈ A ∃* y ∈ B y y ∈ y ∈ B | C ∈ A ⟼ C x
94 91 93 sylibr ⊢ A ∈ Fin ∧ A ≈ B ∧ ∀ x ∈ A ∃ y ∈ B x = C → ∀ x ∈ A ∃* y ∈ B x = C
95 94 ex ⊢ A ∈ Fin ∧ A ≈ B → ∀ x ∈ A ∃ y ∈ B x = C → ∀ x ∈ A ∃* y ∈ B x = C
96 95 pm4.71d ⊢ A ∈ Fin ∧ A ≈ B → ∀ x ∈ A ∃ y ∈ B x = C ↔ ∀ x ∈ A ∃ y ∈ B x = C ∧ ∀ x ∈ A ∃* y ∈ B x = C
97 reu5 ⊢ ∃! y ∈ B x = C ↔ ∃ y ∈ B x = C ∧ ∃* y ∈ B x = C
98 97 ralbii ⊢ ∀ x ∈ A ∃! y ∈ B x = C ↔ ∀ x ∈ A ∃ y ∈ B x = C ∧ ∃* y ∈ B x = C
99 r19.26 ⊢ ∀ x ∈ A ∃ y ∈ B x = C ∧ ∃* y ∈ B x = C ↔ ∀ x ∈ A ∃ y ∈ B x = C ∧ ∀ x ∈ A ∃* y ∈ B x = C
100 98 99 bitri ⊢ ∀ x ∈ A ∃! y ∈ B x = C ↔ ∀ x ∈ A ∃ y ∈ B x = C ∧ ∀ x ∈ A ∃* y ∈ B x = C
101 96 100 bitr4di ⊢ A ∈ Fin ∧ A ≈ B → ∀ x ∈ A ∃ y ∈ B x = C ↔ ∀ x ∈ A ∃! y ∈ B x = C