| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | unieq 4917 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∪ ∅) | 
| 2 |  | uni0 4934 | . . . . . . . . . . 11
⊢ ∪ ∅ = ∅ | 
| 3 | 1, 2 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∅) | 
| 4 | 3 | ineq2d 4219 | . . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) =
(𝑏 ∩
∅)) | 
| 5 |  | in0 4394 | . . . . . . . . 9
⊢ (𝑏 ∩ ∅) =
∅ | 
| 6 | 4, 5 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) =
∅) | 
| 7 | 6 | fveq2d 6909 | . . . . . . 7
⊢ (𝑥 = ∅ →
(♯‘(𝑏 ∩
∪ 𝑥)) =
(♯‘∅)) | 
| 8 |  | hash0 14407 | . . . . . . 7
⊢
(♯‘∅) = 0 | 
| 9 | 7, 8 | eqtrdi 2792 | . . . . . 6
⊢ (𝑥 = ∅ →
(♯‘(𝑏 ∩
∪ 𝑥)) = 0) | 
| 10 | 9 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = ∅ →
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑥))) = ((♯‘𝑏) − 0)) | 
| 11 |  | pweq 4613 | . . . . . . 7
⊢ (𝑥 = ∅ → 𝒫
𝑥 = 𝒫
∅) | 
| 12 |  | pw0 4811 | . . . . . . 7
⊢ 𝒫
∅ = {∅} | 
| 13 | 11, 12 | eqtrdi 2792 | . . . . . 6
⊢ (𝑥 = ∅ → 𝒫
𝑥 =
{∅}) | 
| 14 | 13 | sumeq1d 15737 | . . . . 5
⊢ (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) | 
| 15 | 10, 14 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = ∅ →
(((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− 0) = Σ𝑠
∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) | 
| 16 | 15 | ralbidv 3177 | . . 3
⊢ (𝑥 = ∅ → (∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
0) = Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) | 
| 17 |  | unieq 4917 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → ∪ 𝑥 = ∪
𝑦) | 
| 18 | 17 | ineq2d 4219 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝑦)) | 
| 19 | 18 | fveq2d 6909 | . . . . . 6
⊢ (𝑥 = 𝑦 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝑦))) | 
| 20 | 19 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝑦 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))) | 
| 21 |  | pweq 4613 | . . . . . 6
⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦) | 
| 22 | 21 | sumeq1d 15737 | . . . . 5
⊢ (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) | 
| 23 | 20, 22 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝑦 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− (♯‘(𝑏
∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) | 
| 24 | 23 | ralbidv 3177 | . . 3
⊢ (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥)))
= Σ𝑠 ∈ 𝒫
𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) | 
| 25 |  | unieq 4917 | . . . . . . . . 9
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = ∪
(𝑦 ∪ {𝑧})) | 
| 26 |  | uniun 4929 | . . . . . . . . . 10
⊢ ∪ (𝑦
∪ {𝑧}) = (∪ 𝑦
∪ ∪ {𝑧}) | 
| 27 |  | unisnv 4926 | . . . . . . . . . . 11
⊢ ∪ {𝑧}
= 𝑧 | 
| 28 | 27 | uneq2i 4164 | . . . . . . . . . 10
⊢ (∪ 𝑦
∪ ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧) | 
| 29 | 26, 28 | eqtri 2764 | . . . . . . . . 9
⊢ ∪ (𝑦
∪ {𝑧}) = (∪ 𝑦
∪ 𝑧) | 
| 30 | 25, 29 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = (∪
𝑦 ∪ 𝑧)) | 
| 31 | 30 | ineq2d 4219 | . . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) | 
| 32 | 31 | fveq2d 6909 | . . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ (∪ 𝑦
∪ 𝑧)))) | 
| 33 | 32 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦
∪ 𝑧))))) | 
| 34 |  | pweq 4613 | . . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧})) | 
| 35 | 34 | sumeq1d 15737 | . . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
(𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠)))) | 
| 36 | 33, 35 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− (♯‘(𝑏
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) | 
| 37 | 36 | ralbidv 3177 | . . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥)))
= Σ𝑠 ∈ 𝒫
𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) | 
| 38 |  | unieq 4917 | . . . . . . . 8
⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪
𝐴) | 
| 39 | 38 | ineq2d 4219 | . . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝐴)) | 
| 40 | 39 | fveq2d 6909 | . . . . . 6
⊢ (𝑥 = 𝐴 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝐴))) | 
| 41 | 40 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝐴 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴)))) | 
| 42 |  | pweq 4613 | . . . . . 6
⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) | 
| 43 | 42 | sumeq1d 15737 | . . . . 5
⊢ (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) | 
| 44 | 41, 43 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝐴 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− (♯‘(𝑏
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) | 
| 45 | 44 | ralbidv 3177 | . . 3
⊢ (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥)))
= Σ𝑠 ∈ 𝒫
𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) | 
| 46 |  | hashcl 14396 | . . . . . . 7
⊢ (𝑏 ∈ Fin →
(♯‘𝑏) ∈
ℕ0) | 
| 47 | 46 | nn0cnd 12591 | . . . . . 6
⊢ (𝑏 ∈ Fin →
(♯‘𝑏) ∈
ℂ) | 
| 48 | 47 | mullidd 11280 | . . . . 5
⊢ (𝑏 ∈ Fin → (1 ·
(♯‘𝑏)) =
(♯‘𝑏)) | 
| 49 |  | 0ex 5306 | . . . . . 6
⊢ ∅
∈ V | 
| 50 | 48, 47 | eqeltrd 2840 | . . . . . 6
⊢ (𝑏 ∈ Fin → (1 ·
(♯‘𝑏)) ∈
ℂ) | 
| 51 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑠 = ∅ →
(♯‘𝑠) =
(♯‘∅)) | 
| 52 | 51, 8 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝑠 = ∅ →
(♯‘𝑠) =
0) | 
| 53 | 52 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑠 = ∅ →
(-1↑(♯‘𝑠))
= (-1↑0)) | 
| 54 |  | neg1cn 12381 | . . . . . . . . . 10
⊢ -1 ∈
ℂ | 
| 55 |  | exp0 14107 | . . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑0) = 1) | 
| 56 | 54, 55 | ax-mp 5 | . . . . . . . . 9
⊢
(-1↑0) = 1 | 
| 57 | 53, 56 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑠 = ∅ →
(-1↑(♯‘𝑠))
= 1) | 
| 58 |  | rint0 4987 | . . . . . . . . 9
⊢ (𝑠 = ∅ → (𝑏 ∩ ∩ 𝑠) =
𝑏) | 
| 59 | 58 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑠 = ∅ →
(♯‘(𝑏 ∩
∩ 𝑠)) = (♯‘𝑏)) | 
| 60 | 57, 59 | oveq12d 7450 | . . . . . . 7
⊢ (𝑠 = ∅ →
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= (1 · (♯‘𝑏))) | 
| 61 | 60 | sumsn 15783 | . . . . . 6
⊢ ((∅
∈ V ∧ (1 · (♯‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= (1 · (♯‘𝑏))) | 
| 62 | 49, 50, 61 | sylancr 587 | . . . . 5
⊢ (𝑏 ∈ Fin → Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= (1 · (♯‘𝑏))) | 
| 63 | 47 | subid1d 11610 | . . . . 5
⊢ (𝑏 ∈ Fin →
((♯‘𝑏) −
0) = (♯‘𝑏)) | 
| 64 | 48, 62, 63 | 3eqtr4rd 2787 | . . . 4
⊢ (𝑏 ∈ Fin →
((♯‘𝑏) −
0) = Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) | 
| 65 | 64 | rgen 3062 | . . 3
⊢
∀𝑏 ∈ Fin
((♯‘𝑏) −
0) = Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) | 
| 66 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑥 → (♯‘𝑏) = (♯‘𝑥)) | 
| 67 |  | ineq1 4212 | . . . . . . . . . . . . 13
⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ ∪ 𝑦)) | 
| 68 | 67 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ ∪ 𝑦))) | 
| 69 | 66, 68 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))) | 
| 70 |  | simpl 482 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥) | 
| 71 | 70 | ineq1d 4218 | . . . . . . . . . . . . . 14
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠)) | 
| 72 | 71 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠))) | 
| 73 | 72 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠)))) | 
| 74 | 73 | sumeq2dv 15739 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) | 
| 75 | 69, 74 | eqeq12d 2752 | . . . . . . . . . 10
⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑥)
− (♯‘(𝑥
∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) | 
| 76 | 75 | rspcva 3619 | . . . . . . . . 9
⊢ ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) | 
| 77 | 76 | adantll 714 | . . . . . . . 8
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) | 
| 78 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin) | 
| 79 |  | inss1 4236 | . . . . . . . . . 10
⊢ (𝑥 ∩ 𝑧) ⊆ 𝑥 | 
| 80 |  | ssfi 9214 | . . . . . . . . . 10
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝑧) ⊆ 𝑥) → (𝑥 ∩ 𝑧) ∈ Fin) | 
| 81 | 78, 79, 80 | sylancl 586 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ 𝑧) ∈ Fin) | 
| 82 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘𝑏) = (♯‘(𝑥 ∩ 𝑧))) | 
| 83 |  | ineq1 4212 | . . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦)) | 
| 84 |  | in32 4229 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧) | 
| 85 |  | inass 4227 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ ∪ 𝑦)
∩ 𝑧) = (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) | 
| 86 | 84, 85 | eqtri 2764 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) | 
| 87 | 83, 86 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) | 
| 88 | 87 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧)))) | 
| 89 | 82, 88 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) | 
| 90 |  | ineq1 4212 | . . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠)) | 
| 91 |  | in32 4229 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧) | 
| 92 |  | inass 4227 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∩ ∩ 𝑠)
∩ 𝑧) = (𝑥 ∩ (∩ 𝑠
∩ 𝑧)) | 
| 93 | 91, 92 | eqtri 2764 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) | 
| 94 | 90, 93 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) | 
| 95 | 94 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) | 
| 96 | 95 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) | 
| 97 | 96 | sumeq2sdv 15740 | . . . . . . . . . . 11
⊢ (𝑏 = (𝑥 ∩ 𝑧) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) | 
| 98 | 89, 97 | eqeq12d 2752 | . . . . . . . . . 10
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘(𝑥
∩ 𝑧)) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) | 
| 99 | 98 | rspcva 3619 | . . . . . . . . 9
⊢ (((𝑥 ∩ 𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) | 
| 100 | 81, 99 | sylan 580 | . . . . . . . 8
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) | 
| 101 | 77, 100 | oveq12d 7450 | . . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
− ((♯‘(𝑥
∩ 𝑧)) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) | 
| 102 |  | inss1 4236 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∩ ∪ 𝑦)
⊆ 𝑥 | 
| 103 |  | ssfi 9214 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∪ 𝑦)
⊆ 𝑥) → (𝑥 ∩ ∪ 𝑦)
∈ Fin) | 
| 104 | 78, 102, 103 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ∪ 𝑦) ∈ Fin) | 
| 105 |  | hashcl 14396 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∩ ∪ 𝑦)
∈ Fin → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈
ℕ0) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦))
∈ ℕ0) | 
| 107 | 106 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦))
∈ ℂ) | 
| 108 |  | hashcl 14396 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∩ 𝑧) ∈ Fin → (♯‘(𝑥 ∩ 𝑧)) ∈
ℕ0) | 
| 109 | 81, 108 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈
ℕ0) | 
| 110 | 109 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈ ℂ) | 
| 111 |  | inss1 4236 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) ⊆ 𝑥 | 
| 112 |  | ssfi 9214 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin) | 
| 113 | 78, 111, 112 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin) | 
| 114 |  | hashcl 14396 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∩ (∪ 𝑦
∩ 𝑧)) ∈ Fin →
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧))) ∈
ℕ0) | 
| 115 | 113, 114 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧))) ∈
ℕ0) | 
| 116 | 115 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧))) ∈
ℂ) | 
| 117 |  | hashun3 14424 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∩ ∪ 𝑦)
∈ Fin ∧ (𝑥 ∩
𝑧) ∈ Fin) →
(♯‘((𝑥 ∩
∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦)
∩ (𝑥 ∩ 𝑧))))) | 
| 118 | 104, 81, 117 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘((𝑥 ∩ ∪ 𝑦)
∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦))
+ (♯‘(𝑥 ∩
𝑧))) −
(♯‘((𝑥 ∩
∪ 𝑦) ∩ (𝑥 ∩ 𝑧))))) | 
| 119 |  | indi 4283 | . . . . . . . . . . . . 13
⊢ (𝑥 ∩ (∪ 𝑦
∪ 𝑧)) = ((𝑥 ∩ ∪ 𝑦)
∪ (𝑥 ∩ 𝑧)) | 
| 120 | 119 | fveq2i 6908 | . . . . . . . . . . . 12
⊢
(♯‘(𝑥
∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) | 
| 121 |  | inindi 4234 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) = ((𝑥 ∩ ∪ 𝑦)
∩ (𝑥 ∩ 𝑧)) | 
| 122 | 121 | fveq2i 6908 | . . . . . . . . . . . . 13
⊢
(♯‘(𝑥
∩ (∪ 𝑦 ∩ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))) | 
| 123 | 122 | oveq2i 7443 | . . . . . . . . . . . 12
⊢
(((♯‘(𝑥
∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧)))) =
(((♯‘(𝑥 ∩
∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦)
∩ (𝑥 ∩ 𝑧)))) | 
| 124 | 118, 120,
123 | 3eqtr4g 2801 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧))) =
(((♯‘(𝑥 ∩
∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧))))) | 
| 125 | 107, 110,
116, 124 | assraddsubd 11678 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧))) =
((♯‘(𝑥 ∩
∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))) | 
| 126 | 125 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) =
((♯‘𝑥) −
((♯‘(𝑥 ∩
∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))) | 
| 127 |  | hashcl 14396 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) | 
| 128 | 127 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈
ℕ0) | 
| 129 | 128 | nn0cnd 12591 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈
ℂ) | 
| 130 | 110, 116 | subcld 11621 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) ∈ ℂ) | 
| 131 | 129, 107,
130 | subsub4d 11652 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
− ((♯‘(𝑥
∩ 𝑧)) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧))))) = ((♯‘𝑥) − ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))) | 
| 132 | 126, 131 | eqtr4d 2779 | . . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) =
(((♯‘𝑥) −
(♯‘(𝑥 ∩
∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))) | 
| 133 | 132 | adantr 480 | . . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) =
(((♯‘𝑥) −
(♯‘(𝑥 ∩
∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))) | 
| 134 |  | disjdif 4471 | . . . . . . . . . . 11
⊢
(𝒫 𝑦 ∩
(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅ | 
| 135 | 134 | a1i 11 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅) | 
| 136 |  | ssun1 4177 | . . . . . . . . . . . . . 14
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) | 
| 137 | 136 | sspwi 4611 | . . . . . . . . . . . . 13
⊢ 𝒫
𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) | 
| 138 |  | undif 4481 | . . . . . . . . . . . . 13
⊢
(𝒫 𝑦 ⊆
𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})) | 
| 139 | 137, 138 | mpbi 230 | . . . . . . . . . . . 12
⊢
(𝒫 𝑦 ∪
(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}) | 
| 140 | 139 | eqcomi 2745 | . . . . . . . . . . 11
⊢ 𝒫
(𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) | 
| 141 | 140 | a1i 11 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) | 
| 142 |  | simpll 766 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin) | 
| 143 |  | snfi 9084 | . . . . . . . . . . . 12
⊢ {𝑧} ∈ Fin | 
| 144 |  | unfi 9212 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 145 | 142, 143,
144 | sylancl 586 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 146 |  | pwfi 9358 | . . . . . . . . . . 11
⊢ ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 147 | 145, 146 | sylib 218 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 148 | 54 | a1i 11 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈
ℂ) | 
| 149 |  | elpwi 4606 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧})) | 
| 150 |  | ssfi 9214 | . . . . . . . . . . . . . 14
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin) | 
| 151 | 145, 149,
150 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin) | 
| 152 |  | hashcl 14396 | . . . . . . . . . . . . 13
⊢ (𝑠 ∈ Fin →
(♯‘𝑠) ∈
ℕ0) | 
| 153 | 151, 152 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘𝑠) ∈
ℕ0) | 
| 154 | 148, 153 | expcld 14187 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (-1↑(♯‘𝑠)) ∈
ℂ) | 
| 155 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin) | 
| 156 |  | inss1 4236 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∩ ∩ 𝑠)
⊆ 𝑥 | 
| 157 |  | ssfi 9214 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∩ 𝑠)
⊆ 𝑥) → (𝑥 ∩ ∩ 𝑠)
∈ Fin) | 
| 158 | 155, 156,
157 | sylancl 586 | . . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ∩ 𝑠) ∈ Fin) | 
| 159 |  | hashcl 14396 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∩ ∩ 𝑠)
∈ Fin → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈
ℕ0) | 
| 160 | 158, 159 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈
ℕ0) | 
| 161 | 160 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈
ℂ) | 
| 162 | 154, 161 | mulcld 11282 | . . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) ∈ ℂ) | 
| 163 | 135, 141,
147, 162 | fsumsplit 15778 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= (Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
+ Σ𝑠 ∈
(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))))) | 
| 164 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘𝑠) = (♯‘(𝑡 ∪ {𝑧}))) | 
| 165 | 164 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (-1↑(♯‘𝑠)) =
(-1↑(♯‘(𝑡
∪ {𝑧})))) | 
| 166 |  | inteq 4948 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = ∩
(𝑡 ∪ {𝑧})) | 
| 167 |  | vex 3483 | . . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V | 
| 168 | 167 | intunsn 4986 | . . . . . . . . . . . . . . . 16
⊢ ∩ (𝑡
∪ {𝑧}) = (∩ 𝑡
∩ 𝑧) | 
| 169 | 166, 168 | eqtrdi 2792 | . . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = (∩
𝑡 ∩ 𝑧)) | 
| 170 | 169 | ineq2d 4219 | . . . . . . . . . . . . . 14
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) | 
| 171 | 170 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘(𝑥 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) | 
| 172 | 165, 171 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) = ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧))))) | 
| 173 |  | pwfi 9358 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ Fin ↔ 𝒫
𝑦 ∈
Fin) | 
| 174 | 142, 173 | sylib 218 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin) | 
| 175 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) | 
| 176 |  | elpwi 4606 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ 𝒫 𝑦 → 𝑢 ⊆ 𝑦) | 
| 177 | 176 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢 ⊆ 𝑦) | 
| 178 |  | unss1 4184 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ⊆ 𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) | 
| 179 | 177, 178 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) | 
| 180 |  | vex 3483 | . . . . . . . . . . . . . . . . 17
⊢ 𝑢 ∈ V | 
| 181 |  | vsnex 5433 | . . . . . . . . . . . . . . . . 17
⊢ {𝑧} ∈ V | 
| 182 | 180, 181 | unex 7765 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ∪ {𝑧}) ∈ V | 
| 183 | 182 | elpw 4603 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) | 
| 184 | 179, 183 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧})) | 
| 185 |  | simpllr 775 | . . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦) | 
| 186 |  | elpwi 4606 | . . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦) | 
| 187 |  | ssun2 4178 | . . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧}) | 
| 188 | 167 | snss 4784 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧})) | 
| 189 | 187, 188 | mpbir 231 | . . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ (𝑢 ∪ {𝑧}) | 
| 190 | 189 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧})) | 
| 191 |  | ssel 3976 | . . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧 ∈ 𝑦)) | 
| 192 | 186, 190,
191 | syl2imc 41 | . . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → 𝑧 ∈ 𝑦)) | 
| 193 | 185, 192 | mtod 198 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦) | 
| 194 | 184, 193 | eldifd 3961 | . . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) | 
| 195 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) | 
| 196 | 195 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) | 
| 197 | 196 | elpwid 4608 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧})) | 
| 198 |  | uncom 4157 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦) | 
| 199 | 197, 198 | sseqtrdi 4023 | . . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦)) | 
| 200 |  | ssundif 4487 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦) | 
| 201 | 199, 200 | sylib 218 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦) | 
| 202 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V | 
| 203 | 202 | elpw2 5333 | . . . . . . . . . . . . . 14
⊢ ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦) | 
| 204 | 201, 203 | sylibr 234 | . . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦) | 
| 205 |  | elpwunsn 4683 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧 ∈ 𝑠) | 
| 206 | 205 | ad2antll 729 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧 ∈ 𝑠) | 
| 207 | 206 | snssd 4808 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠) | 
| 208 |  | ssequn2 4188 | . . . . . . . . . . . . . . . . 17
⊢ ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠) | 
| 209 | 207, 208 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠) | 
| 210 | 209 | eqcomd 2742 | . . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧})) | 
| 211 |  | uneq1 4160 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧})) | 
| 212 |  | undif1 4475 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧}) | 
| 213 | 211, 212 | eqtrdi 2792 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧})) | 
| 214 | 213 | eqeq2d 2747 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧}))) | 
| 215 | 210, 214 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧}))) | 
| 216 | 176 | ad2antrl 728 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 ⊆ 𝑦) | 
| 217 |  | simpllr 775 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑦) | 
| 218 | 216, 217 | ssneldd 3985 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑢) | 
| 219 |  | difsnb 4805 | . . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ 𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢) | 
| 220 | 218, 219 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢) | 
| 221 | 220 | eqcomd 2742 | . . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧})) | 
| 222 |  | difeq1 4118 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧})) | 
| 223 |  | difun2 4480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧}) | 
| 224 | 222, 223 | eqtrdi 2792 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧})) | 
| 225 | 224 | eqeq2d 2747 | . . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧}))) | 
| 226 | 221, 225 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧}))) | 
| 227 | 215, 226 | impbid 212 | . . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧}))) | 
| 228 | 175, 194,
204, 227 | f1o2d 7688 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦–1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) | 
| 229 |  | uneq1 4160 | . . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧})) | 
| 230 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑡 ∈ V | 
| 231 | 230, 181 | unex 7765 | . . . . . . . . . . . . . 14
⊢ (𝑡 ∪ {𝑧}) ∈ V | 
| 232 | 229, 175,
231 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧})) | 
| 233 | 232 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧})) | 
| 234 | 195, 162 | sylan2 593 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) ∈ ℂ) | 
| 235 | 172, 174,
228, 233, 234 | fsumf1o 15760 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= Σ𝑡 ∈ 𝒫
𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧))))) | 
| 236 |  | uneq1 4160 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧})) | 
| 237 | 236 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑠 → (♯‘(𝑡 ∪ {𝑧})) = (♯‘(𝑠 ∪ {𝑧}))) | 
| 238 | 237 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (-1↑(♯‘(𝑡 ∪ {𝑧}))) = (-1↑(♯‘(𝑠 ∪ {𝑧})))) | 
| 239 |  | inteq 4948 | . . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑠 → ∩ 𝑡 = ∩
𝑠) | 
| 240 | 239 | ineq1d 4218 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑠 → (∩ 𝑡 ∩ 𝑧) = (∩ 𝑠 ∩ 𝑧)) | 
| 241 | 240 | ineq2d 4219 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑠 → (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) | 
| 242 | 241 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) = (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) | 
| 243 | 238, 242 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) =
((-1↑(♯‘(𝑠
∪ {𝑧}))) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) | 
| 244 | 243 | cbvsumv 15733 | . . . . . . . . . . . 12
⊢
Σ𝑡 ∈
𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) | 
| 245 | 54 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ) | 
| 246 |  | elpwi 4606 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦) | 
| 247 |  | ssfi 9214 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦) → 𝑠 ∈ Fin) | 
| 248 | 142, 246,
247 | syl2an 596 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin) | 
| 249 | 248, 152 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘𝑠) ∈
ℕ0) | 
| 250 | 245, 249 | expp1d 14188 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑((♯‘𝑠) + 1)) =
((-1↑(♯‘𝑠)) · -1)) | 
| 251 | 246 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ⊆ 𝑦) | 
| 252 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦) | 
| 253 | 251, 252 | ssneldd 3985 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑠) | 
| 254 |  | hashunsng 14432 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1))) | 
| 255 | 254 | elv 3484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1)) | 
| 256 | 248, 253,
255 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1)) | 
| 257 | 256 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1↑((♯‘𝑠) + 1))) | 
| 258 | 137 | sseli 3978 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) | 
| 259 | 258, 154 | sylan2 593 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘𝑠)) ∈
ℂ) | 
| 260 | 245, 259 | mulcomd 11283 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 ·
(-1↑(♯‘𝑠))) = ((-1↑(♯‘𝑠)) ·
-1)) | 
| 261 | 250, 257,
260 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1 ·
(-1↑(♯‘𝑠)))) | 
| 262 | 259 | mulm1d 11716 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 ·
(-1↑(♯‘𝑠))) = -(-1↑(♯‘𝑠))) | 
| 263 | 261, 262 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = -(-1↑(♯‘𝑠))) | 
| 264 | 263 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) =
(-(-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) | 
| 265 |  | inss1 4236 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∩ (∩ 𝑠
∩ 𝑧)) ⊆ 𝑥 | 
| 266 |  | ssfi 9214 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∩ 𝑠
∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin) | 
| 267 | 155, 265,
266 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin) | 
| 268 |  | hashcl 14396 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∩ (∩ 𝑠
∩ 𝑧)) ∈ Fin →
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))) ∈
ℕ0) | 
| 269 | 267, 268 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈
ℕ0) | 
| 270 | 269 | nn0cnd 12591 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ) | 
| 271 | 258, 270 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ) | 
| 272 | 259, 271 | mulneg1d 11717 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-(-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) = -((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) | 
| 273 | 264, 272 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) =
-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) | 
| 274 | 273 | sumeq2dv 15739 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) | 
| 275 | 244, 274 | eqtrid 2788 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) | 
| 276 | 154, 270 | mulcld 11282 | . . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) ∈ ℂ) | 
| 277 | 258, 276 | sylan2 593 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) ∈ ℂ) | 
| 278 | 174, 277 | fsumneg 15824 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) | 
| 279 | 235, 275,
278 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= -Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) | 
| 280 | 279 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
+ -Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) | 
| 281 | 137 | a1i 11 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})) | 
| 282 | 281 | sselda 3982 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) | 
| 283 | 282, 162 | syldan 591 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) ∈ ℂ) | 
| 284 | 174, 283 | fsumcl 15770 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
∈ ℂ) | 
| 285 | 282, 276 | syldan 591 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) ∈ ℂ) | 
| 286 | 174, 285 | fsumcl 15770 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) ∈
ℂ) | 
| 287 | 284, 286 | negsubd 11627 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) =
(Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) | 
| 288 | 163, 280,
287 | 3eqtrd 2780 | . . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= (Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) | 
| 289 | 288 | adantr 480 | . . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= (Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) | 
| 290 | 101, 133,
289 | 3eqtr4d 2786 | . . . . . 6
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) | 
| 291 | 290 | ex 412 | . . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
→ ((♯‘𝑥)
− (♯‘(𝑥
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) | 
| 292 | 291 | ralrimdva 3153 | . . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
→ ∀𝑥 ∈ Fin
((♯‘𝑥) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) | 
| 293 |  | ineq1 4212 | . . . . . . . 8
⊢ (𝑏 = 𝑥 → (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)) = (𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) | 
| 294 | 293 | fveq2d 6909 | . . . . . . 7
⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) | 
| 295 | 66, 294 | oveq12d 7450 | . . . . . 6
⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))))) | 
| 296 |  | ineq1 4212 | . . . . . . . . 9
⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠)) | 
| 297 | 296 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠))) | 
| 298 | 297 | oveq2d 7448 | . . . . . . 7
⊢ (𝑏 = 𝑥 → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠)))) | 
| 299 | 298 | sumeq2sdv 15740 | . . . . . 6
⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
(𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠)))) | 
| 300 | 295, 299 | eqeq12d 2752 | . . . . 5
⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑥)
− (♯‘(𝑥
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) | 
| 301 | 300 | cbvralvw 3236 | . . . 4
⊢
(∀𝑏 ∈
Fin ((♯‘𝑏)
− (♯‘(𝑏
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑥 ∈ Fin
((♯‘𝑥) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) | 
| 302 | 292, 301 | imbitrrdi 252 | . . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
→ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) | 
| 303 | 16, 24, 37, 45, 65, 302 | findcard2s 9206 | . 2
⊢ (𝐴 ∈ Fin → ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) | 
| 304 |  | fveq2 6905 | . . . . 5
⊢ (𝑏 = 𝐵 → (♯‘𝑏) = (♯‘𝐵)) | 
| 305 |  | ineq1 4212 | . . . . . 6
⊢ (𝑏 = 𝐵 → (𝑏 ∩ ∪ 𝐴) = (𝐵 ∩ ∪ 𝐴)) | 
| 306 | 305 | fveq2d 6909 | . . . . 5
⊢ (𝑏 = 𝐵 → (♯‘(𝑏 ∩ ∪ 𝐴)) = (♯‘(𝐵 ∩ ∪ 𝐴))) | 
| 307 | 304, 306 | oveq12d 7450 | . . . 4
⊢ (𝑏 = 𝐵 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴)))) | 
| 308 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵) | 
| 309 | 308 | ineq1d 4218 | . . . . . . 7
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (𝑏 ∩ ∩ 𝑠) = (𝐵 ∩ ∩ 𝑠)) | 
| 310 | 309 | fveq2d 6909 | . . . . . 6
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝐵 ∩ ∩ 𝑠))) | 
| 311 | 310 | oveq2d 7448 | . . . . 5
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝐵 ∩
∩ 𝑠)))) | 
| 312 | 311 | sumeq2dv 15739 | . . . 4
⊢ (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) | 
| 313 | 307, 312 | eqeq12d 2752 | . . 3
⊢ (𝑏 = 𝐵 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝐵)
− (♯‘(𝐵
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))) | 
| 314 | 313 | rspccva 3620 | . 2
⊢
((∀𝑏 ∈
Fin ((♯‘𝑏)
− (♯‘(𝑏
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
∧ 𝐵 ∈ Fin) →
((♯‘𝐵) −
(♯‘(𝐵 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) | 
| 315 | 303, 314 | sylan 580 | 1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐵) −
(♯‘(𝐵 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) |