Metamath Proof Explorer

Theorem ballotlem7

Description: R is a bijection between two subsets of ( O \ E ) : one where a vote for A is picked first, and one where a vote for B is picked first. (Contributed by Thierry Arnoux, 12-Dec-2016)

Ref Expression
Hypotheses ballotth.m ⊢M∈ℕ
ballotth.n ⊢N∈ℕ
ballotth.o ⊢O=c∈𝒫1…M+N|c=M
ballotth.p ⊢P=x∈𝒫O⟼xO
ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
ballotth.mgtn ⊢N<M
ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
ballotth.r ⊢R=c∈O∖E⟼S⁡cc
Assertion ballotlem7 ⊢R↾c∈O∖E|1∈c:c∈O∖E|1∈c⟶1-1 ontoc∈O∖E|¬1∈c

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢M∈ℕ
2 ballotth.n ⊢N∈ℕ
3 ballotth.o ⊢O=c∈𝒫1…M+N|c=M
4 ballotth.p ⊢P=x∈𝒫O⟼xO
5 ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
6 ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
7 ballotth.mgtn ⊢N<M
8 ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
9 ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
10 ballotth.r ⊢R=c∈O∖E⟼S⁡cc
11 10 funmpt2 ⊢Fun⁡R
12 1 2 3 4 5 6 7 8 9 10 ballotlemrinv ⊢R-1=R
13 rabid ⊢c∈c∈O∖E|1∈c↔c∈O∖E∧1∈c
14 1 2 3 4 5 6 7 8 9 10 ballotlemrc ⊢c∈O∖E→R⁡c∈O∖E
15 14 adantr ⊢c∈O∖E∧1∈c→R⁡c∈O∖E
16 1 2 3 4 5 6 7 8 ballotlem1c ⊢c∈O∖E∧1∈c→¬I⁡c∈c
17 16 ex ⊢c∈O∖E→1∈c→¬I⁡c∈c
18 1 2 3 4 5 6 7 8 9 10 ballotlem1ri ⊢c∈O∖E→1∈R⁡c↔I⁡c∈c
19 18 notbid ⊢c∈O∖E→¬1∈R⁡c↔¬I⁡c∈c
20 17 19 sylibrd ⊢c∈O∖E→1∈c→¬1∈R⁡c
21 20 imp ⊢c∈O∖E∧1∈c→¬1∈R⁡c
22 15 21 jca ⊢c∈O∖E∧1∈c→R⁡c∈O∖E∧¬1∈R⁡c
23 13 22 sylbi ⊢c∈c∈O∖E|1∈c→R⁡c∈O∖E∧¬1∈R⁡c
24 23 rgen ⊢∀c∈c∈O∖E|1∈cR⁡c∈O∖E∧¬1∈R⁡c
25 eleq2 ⊢b=R⁡c→1∈b↔1∈R⁡c
26 25 notbid ⊢b=R⁡c→¬1∈b↔¬1∈R⁡c
27 26 elrab ⊢R⁡c∈b∈O∖E|¬1∈b↔R⁡c∈O∖E∧¬1∈R⁡c
28 eleq2 ⊢b=c→1∈b↔1∈c
29 28 notbid ⊢b=c→¬1∈b↔¬1∈c
30 29 cbvrabv ⊢b∈O∖E|¬1∈b=c∈O∖E|¬1∈c
31 30 eleq2i ⊢R⁡c∈b∈O∖E|¬1∈b↔R⁡c∈c∈O∖E|¬1∈c
32 27 31 bitr3i ⊢R⁡c∈O∖E∧¬1∈R⁡c↔R⁡c∈c∈O∖E|¬1∈c
33 32 ralbii ⊢∀c∈c∈O∖E|1∈cR⁡c∈O∖E∧¬1∈R⁡c↔∀c∈c∈O∖E|1∈cR⁡c∈c∈O∖E|¬1∈c
34 24 33 mpbi ⊢∀c∈c∈O∖E|1∈cR⁡c∈c∈O∖E|¬1∈c
35 ssrab2 ⊢c∈O∖E|1∈c⊆O∖E
36 fvex ⊢S⁡c∈V
37 imaexg ⊢S⁡c∈V→S⁡cc∈V
38 36 37 ax-mp ⊢S⁡cc∈V
39 38 10 dmmpti ⊢dom⁡R=O∖E
40 35 39 sseqtrri ⊢c∈O∖E|1∈c⊆dom⁡R
41 nfrab1 ⊢Ⅎ_cc∈O∖E|1∈c
42 nfrab1 ⊢Ⅎ_cc∈O∖E|¬1∈c
43 nfmpt1 ⊢Ⅎ_cc∈O∖E⟼S⁡cc
44 10 43 nfcxfr ⊢Ⅎ_cR
45 41 42 44 funimass4f ⊢Fun⁡R∧c∈O∖E|1∈c⊆dom⁡R→Rc∈O∖E|1∈c⊆c∈O∖E|¬1∈c↔∀c∈c∈O∖E|1∈cR⁡c∈c∈O∖E|¬1∈c
46 11 40 45 mp2an ⊢Rc∈O∖E|1∈c⊆c∈O∖E|¬1∈c↔∀c∈c∈O∖E|1∈cR⁡c∈c∈O∖E|¬1∈c
47 34 46 mpbir ⊢Rc∈O∖E|1∈c⊆c∈O∖E|¬1∈c
48 rabid ⊢c∈c∈O∖E|¬1∈c↔c∈O∖E∧¬1∈c
49 14 adantr ⊢c∈O∖E∧¬1∈c→R⁡c∈O∖E
50 1 2 3 4 5 6 7 8 ballotlemic ⊢c∈O∖E∧¬1∈c→I⁡c∈c
51 50 ex ⊢c∈O∖E→¬1∈c→I⁡c∈c
52 51 18 sylibrd ⊢c∈O∖E→¬1∈c→1∈R⁡c
53 52 imp ⊢c∈O∖E∧¬1∈c→1∈R⁡c
54 49 53 jca ⊢c∈O∖E∧¬1∈c→R⁡c∈O∖E∧1∈R⁡c
55 48 54 sylbi ⊢c∈c∈O∖E|¬1∈c→R⁡c∈O∖E∧1∈R⁡c
56 55 rgen ⊢∀c∈c∈O∖E|¬1∈cR⁡c∈O∖E∧1∈R⁡c
57 25 elrab ⊢R⁡c∈b∈O∖E|1∈b↔R⁡c∈O∖E∧1∈R⁡c
58 28 cbvrabv ⊢b∈O∖E|1∈b=c∈O∖E|1∈c
59 58 eleq2i ⊢R⁡c∈b∈O∖E|1∈b↔R⁡c∈c∈O∖E|1∈c
60 57 59 bitr3i ⊢R⁡c∈O∖E∧1∈R⁡c↔R⁡c∈c∈O∖E|1∈c
61 60 ralbii ⊢∀c∈c∈O∖E|¬1∈cR⁡c∈O∖E∧1∈R⁡c↔∀c∈c∈O∖E|¬1∈cR⁡c∈c∈O∖E|1∈c
62 56 61 mpbi ⊢∀c∈c∈O∖E|¬1∈cR⁡c∈c∈O∖E|1∈c
63 ssrab2 ⊢c∈O∖E|¬1∈c⊆O∖E
64 63 39 sseqtrri ⊢c∈O∖E|¬1∈c⊆dom⁡R
65 42 41 44 funimass4f ⊢Fun⁡R∧c∈O∖E|¬1∈c⊆dom⁡R→Rc∈O∖E|¬1∈c⊆c∈O∖E|1∈c↔∀c∈c∈O∖E|¬1∈cR⁡c∈c∈O∖E|1∈c
66 11 64 65 mp2an ⊢Rc∈O∖E|¬1∈c⊆c∈O∖E|1∈c↔∀c∈c∈O∖E|¬1∈cR⁡c∈c∈O∖E|1∈c
67 62 66 mpbir ⊢Rc∈O∖E|¬1∈c⊆c∈O∖E|1∈c
68 11 12 47 67 40 64 rinvf1o ⊢R↾c∈O∖E|1∈c:c∈O∖E|1∈c⟶1-1 ontoc∈O∖E|¬1∈c