| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ballotlemfval.c | . . 3
⊢ (𝜑 → 𝐶 ∈ 𝑂) | 
| 2 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → 𝑏 = 𝐶) | 
| 3 | 2 | ineq2d 4219 | . . . . . . 7
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → ((1...𝑖) ∩ 𝑏) = ((1...𝑖) ∩ 𝐶)) | 
| 4 | 3 | fveq2d 6909 | . . . . . 6
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) →
(♯‘((1...𝑖)
∩ 𝑏)) =
(♯‘((1...𝑖)
∩ 𝐶))) | 
| 5 | 2 | difeq2d 4125 | . . . . . . 7
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → ((1...𝑖) ∖ 𝑏) = ((1...𝑖) ∖ 𝐶)) | 
| 6 | 5 | fveq2d 6909 | . . . . . 6
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) →
(♯‘((1...𝑖)
∖ 𝑏)) =
(♯‘((1...𝑖)
∖ 𝐶))) | 
| 7 | 4, 6 | oveq12d 7450 | . . . . 5
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) →
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏))) =
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶)))) | 
| 8 | 7 | mpteq2dva 5241 | . . . 4
⊢ (𝑏 = 𝐶 → (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏)))) = (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶))))) | 
| 9 |  | ballotth.f | . . . . 5
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) | 
| 10 |  | ineq2 4213 | . . . . . . . . 9
⊢ (𝑏 = 𝑐 → ((1...𝑖) ∩ 𝑏) = ((1...𝑖) ∩ 𝑐)) | 
| 11 | 10 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑏 = 𝑐 → (♯‘((1...𝑖) ∩ 𝑏)) = (♯‘((1...𝑖) ∩ 𝑐))) | 
| 12 |  | difeq2 4119 | . . . . . . . . 9
⊢ (𝑏 = 𝑐 → ((1...𝑖) ∖ 𝑏) = ((1...𝑖) ∖ 𝑐)) | 
| 13 | 12 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑏 = 𝑐 → (♯‘((1...𝑖) ∖ 𝑏)) = (♯‘((1...𝑖) ∖ 𝑐))) | 
| 14 | 11, 13 | oveq12d 7450 | . . . . . . 7
⊢ (𝑏 = 𝑐 → ((♯‘((1...𝑖) ∩ 𝑏)) − (♯‘((1...𝑖) ∖ 𝑏))) = ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))) | 
| 15 | 14 | mpteq2dv 5243 | . . . . . 6
⊢ (𝑏 = 𝑐 → (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏)))) = (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) | 
| 16 | 15 | cbvmptv 5254 | . . . . 5
⊢ (𝑏 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏))))) = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) | 
| 17 | 9, 16 | eqtr4i 2767 | . . . 4
⊢ 𝐹 = (𝑏 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏))))) | 
| 18 |  | zex 12624 | . . . . 5
⊢ ℤ
∈ V | 
| 19 | 18 | mptex 7244 | . . . 4
⊢ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶)))) ∈
V | 
| 20 | 8, 17, 19 | fvmpt 7015 | . . 3
⊢ (𝐶 ∈ 𝑂 → (𝐹‘𝐶) = (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶))))) | 
| 21 | 1, 20 | syl 17 | . 2
⊢ (𝜑 → (𝐹‘𝐶) = (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶))))) | 
| 22 |  | oveq2 7440 | . . . . . 6
⊢ (𝑖 = 𝐽 → (1...𝑖) = (1...𝐽)) | 
| 23 | 22 | ineq1d 4218 | . . . . 5
⊢ (𝑖 = 𝐽 → ((1...𝑖) ∩ 𝐶) = ((1...𝐽) ∩ 𝐶)) | 
| 24 | 23 | fveq2d 6909 | . . . 4
⊢ (𝑖 = 𝐽 → (♯‘((1...𝑖) ∩ 𝐶)) = (♯‘((1...𝐽) ∩ 𝐶))) | 
| 25 | 22 | difeq1d 4124 | . . . . 5
⊢ (𝑖 = 𝐽 → ((1...𝑖) ∖ 𝐶) = ((1...𝐽) ∖ 𝐶)) | 
| 26 | 25 | fveq2d 6909 | . . . 4
⊢ (𝑖 = 𝐽 → (♯‘((1...𝑖) ∖ 𝐶)) = (♯‘((1...𝐽) ∖ 𝐶))) | 
| 27 | 24, 26 | oveq12d 7450 | . . 3
⊢ (𝑖 = 𝐽 → ((♯‘((1...𝑖) ∩ 𝐶)) − (♯‘((1...𝑖) ∖ 𝐶))) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) | 
| 28 | 27 | adantl 481 | . 2
⊢ ((𝜑 ∧ 𝑖 = 𝐽) → ((♯‘((1...𝑖) ∩ 𝐶)) − (♯‘((1...𝑖) ∖ 𝐶))) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) | 
| 29 |  | ballotlemfval.j | . 2
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 30 |  | ovexd 7467 | . 2
⊢ (𝜑 →
((♯‘((1...𝐽)
∩ 𝐶)) −
(♯‘((1...𝐽)
∖ 𝐶))) ∈
V) | 
| 31 | 21, 28, 29, 30 | fvmptd 7022 | 1
⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) |