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 ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
ballotth.mgtn ⊢ 𝑁 < 𝑀
ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
Assertion ballotlem7 ( 𝑅 ↾ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) : { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } –1-1-onto→ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 }

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
7 ballotth.mgtn ⊢ 𝑁 < 𝑀
8 ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
9 ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
11 10 funmpt2 ⊢ Fun 𝑅
12 1 2 3 4 5 6 7 8 9 10 ballotlemrinv ⊢ ◡ 𝑅 = 𝑅
13 rabid ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ↔ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝑐 ) )
14 1 2 3 4 5 6 7 8 9 10 ballotlemrc ⊢ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) )
15 14 adantr ⊢ ( ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝑐 ) → ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) )
16 1 2 3 4 5 6 7 8 ballotlem1c ⊢ ( ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝑐 ) → ¬ ( 𝐼 ‘ 𝑐 ) ∈ 𝑐 )
17 16 ex ⊢ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) → ( 1 ∈ 𝑐 → ¬ ( 𝐼 ‘ 𝑐 ) ∈ 𝑐 ) )
18 1 2 3 4 5 6 7 8 9 10 ballotlem1ri ⊢ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) → ( 1 ∈ ( 𝑅 ‘ 𝑐 ) ↔ ( 𝐼 ‘ 𝑐 ) ∈ 𝑐 ) )
19 18 notbid ⊢ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) → ( ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) ↔ ¬ ( 𝐼 ‘ 𝑐 ) ∈ 𝑐 ) )
20 17 19 sylibrd ⊢ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) → ( 1 ∈ 𝑐 → ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
21 20 imp ⊢ ( ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝑐 ) → ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) )
22 15 21 jca ⊢ ( ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝑐 ) → ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
23 13 22 sylbi ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } → ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
24 23 rgen ⊢ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) )
25 eleq2 ⊢ ( 𝑏 = ( 𝑅 ‘ 𝑐 ) → ( 1 ∈ 𝑏 ↔ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
26 25 notbid ⊢ ( 𝑏 = ( 𝑅 ‘ 𝑐 ) → ( ¬ 1 ∈ 𝑏 ↔ ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
27 26 elrab ⊢ ( ( 𝑅 ‘ 𝑐 ) ∈ { 𝑏 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑏 } ↔ ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
28 eleq2 ⊢ ( 𝑏 = 𝑐 → ( 1 ∈ 𝑏 ↔ 1 ∈ 𝑐 ) )
29 28 notbid ⊢ ( 𝑏 = 𝑐 → ( ¬ 1 ∈ 𝑏 ↔ ¬ 1 ∈ 𝑐 ) )
30 29 cbvrabv ⊢ { 𝑏 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑏 } = { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 }
31 30 eleq2i ⊢ ( ( 𝑅 ‘ 𝑐 ) ∈ { 𝑏 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑏 } ↔ ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } )
32 27 31 bitr3i ⊢ ( ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) ↔ ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } )
33 32 ralbii ⊢ ( ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) ↔ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } )
34 24 33 mpbi ⊢ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 }
35 ssrab2 ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ⊆ ( 𝑂 ∖ 𝐸 )
36 fvex ⊢ ( 𝑆 ‘ 𝑐 ) ∈ V
37 imaexg ⊢ ( ( 𝑆 ‘ 𝑐 ) ∈ V → ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) ∈ V )
38 36 37 ax-mp ⊢ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) ∈ V
39 38 10 dmmpti ⊢ dom 𝑅 = ( 𝑂 ∖ 𝐸 )
40 35 39 sseqtrri ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ⊆ dom 𝑅
41 nfrab1 ⊢ Ⅎ 𝑐 { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 }
42 nfrab1 ⊢ Ⅎ 𝑐 { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 }
43 nfmpt1 ⊢ Ⅎ 𝑐 ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
44 10 43 nfcxfr ⊢ Ⅎ 𝑐 𝑅
45 41 42 44 funimass4f ⊢ ( ( Fun 𝑅 ∧ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ⊆ dom 𝑅 ) → ( ( 𝑅 “ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) ⊆ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ↔ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) )
46 11 40 45 mp2an ⊢ ( ( 𝑅 “ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) ⊆ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ↔ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } )
47 34 46 mpbir ⊢ ( 𝑅 “ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) ⊆ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 }
48 rabid ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ↔ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝑐 ) )
49 14 adantr ⊢ ( ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝑐 ) → ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) )
50 1 2 3 4 5 6 7 8 ballotlemic ⊢ ( ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝑐 ) → ( 𝐼 ‘ 𝑐 ) ∈ 𝑐 )
51 50 ex ⊢ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) → ( ¬ 1 ∈ 𝑐 → ( 𝐼 ‘ 𝑐 ) ∈ 𝑐 ) )
52 51 18 sylibrd ⊢ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) → ( ¬ 1 ∈ 𝑐 → 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
53 52 imp ⊢ ( ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝑐 ) → 1 ∈ ( 𝑅 ‘ 𝑐 ) )
54 49 53 jca ⊢ ( ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝑐 ) → ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
55 48 54 sylbi ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } → ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
56 55 rgen ⊢ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ ( 𝑅 ‘ 𝑐 ) )
57 25 elrab ⊢ ( ( 𝑅 ‘ 𝑐 ) ∈ { 𝑏 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑏 } ↔ ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) )
58 28 cbvrabv ⊢ { 𝑏 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑏 } = { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 }
59 58 eleq2i ⊢ ( ( 𝑅 ‘ 𝑐 ) ∈ { 𝑏 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑏 } ↔ ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } )
60 57 59 bitr3i ⊢ ( ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) ↔ ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } )
61 60 ralbii ⊢ ( ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ( ( 𝑅 ‘ 𝑐 ) ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ ( 𝑅 ‘ 𝑐 ) ) ↔ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } )
62 56 61 mpbi ⊢ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 }
63 ssrab2 ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ⊆ ( 𝑂 ∖ 𝐸 )
64 63 39 sseqtrri ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ⊆ dom 𝑅
65 42 41 44 funimass4f ⊢ ( ( Fun 𝑅 ∧ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ⊆ dom 𝑅 ) → ( ( 𝑅 “ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ⊆ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ↔ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) )
66 11 64 65 mp2an ⊢ ( ( 𝑅 “ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ⊆ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ↔ ∀ 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ( 𝑅 ‘ 𝑐 ) ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } )
67 62 66 mpbir ⊢ ( 𝑅 “ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ⊆ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 }
68 11 12 47 67 40 64 rinvf1o ⊢ ( 𝑅 ↾ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) : { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } –1-1-onto→ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 }