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