Proof of Theorem incexc
| Step | Hyp | Ref
| Expression |
| 1 | | unifi 9384 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴
∈ Fin) |
| 2 | | hashcl 14395 |
. . . 4
⊢ (∪ 𝐴
∈ Fin → (♯‘∪ 𝐴) ∈
ℕ0) |
| 3 | 2 | nn0cnd 12589 |
. . 3
⊢ (∪ 𝐴
∈ Fin → (♯‘∪ 𝐴) ∈ ℂ) |
| 4 | 1, 3 | syl 17 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(♯‘∪ 𝐴) ∈ ℂ) |
| 5 | | simpl 482 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin) |
| 6 | | pwfi 9357 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
| 7 | 5, 6 | sylib 218 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫
𝐴 ∈
Fin) |
| 8 | | diffi 9215 |
. . . 4
⊢
(𝒫 𝐴 ∈
Fin → (𝒫 𝐴
∖ {∅}) ∈ Fin) |
| 9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫
𝐴 ∖ {∅}) ∈
Fin) |
| 10 | | 1cnd 11256 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 1
∈ ℂ) |
| 11 | 10 | negcld 11607 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -1
∈ ℂ) |
| 12 | | eldifsni 4790 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ≠ ∅) |
| 13 | 12 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ≠
∅) |
| 14 | | eldifi 4131 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ∈ 𝒫 𝐴) |
| 15 | | elpwi 4607 |
. . . . . . . . . 10
⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ⊆ 𝐴) |
| 17 | | ssfi 9213 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin) |
| 18 | 5, 16, 17 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ∈
Fin) |
| 19 | | hashnncl 14405 |
. . . . . . . 8
⊢ (𝑠 ∈ Fin →
((♯‘𝑠) ∈
ℕ ↔ 𝑠 ≠
∅)) |
| 20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((♯‘𝑠) ∈
ℕ ↔ 𝑠 ≠
∅)) |
| 21 | 13, 20 | mpbird 257 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(♯‘𝑠) ∈
ℕ) |
| 22 | | nnm1nn0 12567 |
. . . . . 6
⊢
((♯‘𝑠)
∈ ℕ → ((♯‘𝑠) − 1) ∈
ℕ0) |
| 23 | 21, 22 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((♯‘𝑠) −
1) ∈ ℕ0) |
| 24 | 11, 23 | expcld 14186 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-1↑((♯‘𝑠)
− 1)) ∈ ℂ) |
| 25 | 16 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ⊆ 𝐴) |
| 26 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝐴 ⊆
Fin) |
| 27 | 25, 26 | sstrd 3994 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ⊆
Fin) |
| 28 | | unifi 9384 |
. . . . . . . 8
⊢ ((𝑠 ∈ Fin ∧ 𝑠 ⊆ Fin) → ∪ 𝑠
∈ Fin) |
| 29 | 18, 27, 28 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∪ 𝑠 ∈ Fin) |
| 30 | | intssuni 4970 |
. . . . . . . 8
⊢ (𝑠 ≠ ∅ → ∩ 𝑠
⊆ ∪ 𝑠) |
| 31 | 13, 30 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∩ 𝑠 ⊆ ∪ 𝑠) |
| 32 | 29, 31 | ssfid 9301 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∩ 𝑠 ∈ Fin) |
| 33 | | hashcl 14395 |
. . . . . 6
⊢ (∩ 𝑠
∈ Fin → (♯‘∩ 𝑠) ∈
ℕ0) |
| 34 | 32, 33 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(♯‘∩ 𝑠) ∈
ℕ0) |
| 35 | 34 | nn0cnd 12589 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(♯‘∩ 𝑠) ∈ ℂ) |
| 36 | 24, 35 | mulcld 11281 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))
∈ ℂ) |
| 37 | 9, 36 | fsumcl 15769 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))
∈ ℂ) |
| 38 | | disjdif 4472 |
. . . . 5
⊢
({∅} ∩ (𝒫 𝐴 ∖ {∅})) =
∅ |
| 39 | 38 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ({∅}
∩ (𝒫 𝐴 ∖
{∅})) = ∅) |
| 40 | | 0elpw 5356 |
. . . . . . . 8
⊢ ∅
∈ 𝒫 𝐴 |
| 41 | | snssi 4808 |
. . . . . . . 8
⊢ (∅
∈ 𝒫 𝐴 →
{∅} ⊆ 𝒫 𝐴) |
| 42 | 40, 41 | ax-mp 5 |
. . . . . . 7
⊢ {∅}
⊆ 𝒫 𝐴 |
| 43 | | undif 4482 |
. . . . . . 7
⊢
({∅} ⊆ 𝒫 𝐴 ↔ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫
𝐴) |
| 44 | 42, 43 | mpbi 230 |
. . . . . 6
⊢
({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴 |
| 45 | 44 | eqcomi 2746 |
. . . . 5
⊢ 𝒫
𝐴 = ({∅} ∪
(𝒫 𝐴 ∖
{∅})) |
| 46 | 45 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫
𝐴 = ({∅} ∪
(𝒫 𝐴 ∖
{∅}))) |
| 47 | | 1cnd 11256 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 1 ∈
ℂ) |
| 48 | 47 | negcld 11607 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → -1 ∈
ℂ) |
| 49 | 5, 15, 17 | syl2an 596 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑠 ∈ Fin) |
| 50 | | hashcl 14395 |
. . . . . . 7
⊢ (𝑠 ∈ Fin →
(♯‘𝑠) ∈
ℕ0) |
| 51 | 49, 50 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘𝑠) ∈
ℕ0) |
| 52 | 48, 51 | expcld 14186 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) →
(-1↑(♯‘𝑠))
∈ ℂ) |
| 53 | 1 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ∪ 𝐴
∈ Fin) |
| 54 | | inss1 4237 |
. . . . . . . 8
⊢ (∪ 𝐴
∩ ∩ 𝑠) ⊆ ∪ 𝐴 |
| 55 | | ssfi 9213 |
. . . . . . . 8
⊢ ((∪ 𝐴
∈ Fin ∧ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴)
→ (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin) |
| 56 | 53, 54, 55 | sylancl 586 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (∪ 𝐴
∩ ∩ 𝑠) ∈ Fin) |
| 57 | | hashcl 14395 |
. . . . . . 7
⊢ ((∪ 𝐴
∩ ∩ 𝑠) ∈ Fin → (♯‘(∪ 𝐴
∩ ∩ 𝑠)) ∈
ℕ0) |
| 58 | 56, 57 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴
∩ ∩ 𝑠)) ∈
ℕ0) |
| 59 | 58 | nn0cnd 12589 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴
∩ ∩ 𝑠)) ∈ ℂ) |
| 60 | 52, 59 | mulcld 11281 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) →
((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))) ∈ ℂ) |
| 61 | 39, 46, 7, 60 | fsumsplit 15777 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ 𝒫
𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))) = (Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))))) |
| 62 | | inidm 4227 |
. . . . . . 7
⊢ (∪ 𝐴
∩ ∪ 𝐴) = ∪ 𝐴 |
| 63 | 62 | fveq2i 6909 |
. . . . . 6
⊢
(♯‘(∪ 𝐴 ∩ ∪ 𝐴)) = (♯‘∪ 𝐴) |
| 64 | 63 | oveq2i 7442 |
. . . . 5
⊢
((♯‘∪ 𝐴) − (♯‘(∪ 𝐴
∩ ∪ 𝐴))) = ((♯‘∪ 𝐴)
− (♯‘∪ 𝐴)) |
| 65 | 4 | subidd 11608 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((♯‘∪ 𝐴) − (♯‘∪ 𝐴))
= 0) |
| 66 | 64, 65 | eqtrid 2789 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((♯‘∪ 𝐴) − (♯‘(∪ 𝐴
∩ ∪ 𝐴))) = 0) |
| 67 | | incexclem 15872 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ ∪ 𝐴
∈ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠)))) |
| 68 | 1, 67 | syldan 591 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((♯‘∪ 𝐴) − (♯‘(∪ 𝐴
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠)))) |
| 69 | 66, 68 | eqtr3d 2779 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 0 =
Σ𝑠 ∈ 𝒫
𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠)))) |
| 70 | 4, 37 | negsubd 11626 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
= ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))) |
| 71 | | 0ex 5307 |
. . . . . . 7
⊢ ∅
∈ V |
| 72 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 1 ∈
ℂ) |
| 73 | 72, 4 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 ·
(♯‘∪ 𝐴)) ∈ ℂ) |
| 74 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑠 = ∅ →
(♯‘𝑠) =
(♯‘∅)) |
| 75 | | hash0 14406 |
. . . . . . . . . . . 12
⊢
(♯‘∅) = 0 |
| 76 | 74, 75 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑠 = ∅ →
(♯‘𝑠) =
0) |
| 77 | 76 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ →
(-1↑(♯‘𝑠))
= (-1↑0)) |
| 78 | | neg1cn 12380 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
| 79 | | exp0 14106 |
. . . . . . . . . . 11
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
| 80 | 78, 79 | ax-mp 5 |
. . . . . . . . . 10
⊢
(-1↑0) = 1 |
| 81 | 77, 80 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑠 = ∅ →
(-1↑(♯‘𝑠))
= 1) |
| 82 | | rint0 4988 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ → (∪ 𝐴
∩ ∩ 𝑠) = ∪ 𝐴) |
| 83 | 82 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑠 = ∅ →
(♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∪ 𝐴)) |
| 84 | 81, 83 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑠 = ∅ →
((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴))) |
| 85 | 84 | sumsn 15782 |
. . . . . . 7
⊢ ((∅
∈ V ∧ (1 · (♯‘∪ 𝐴)) ∈ ℂ) →
Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴))) |
| 86 | 71, 73, 85 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴))) |
| 87 | 4 | mullidd 11279 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 ·
(♯‘∪ 𝐴)) = (♯‘∪ 𝐴)) |
| 88 | 86, 87 | eqtr2d 2778 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(♯‘∪ 𝐴) = Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠)))) |
| 89 | 9, 36 | fsumneg 15823 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))
= -Σ𝑠 ∈
(𝒫 𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) |
| 90 | | expm1t 14131 |
. . . . . . . . . . 11
⊢ ((-1
∈ ℂ ∧ (♯‘𝑠) ∈ ℕ) →
(-1↑(♯‘𝑠))
= ((-1↑((♯‘𝑠) − 1)) · -1)) |
| 91 | 11, 21, 90 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-1↑(♯‘𝑠))
= ((-1↑((♯‘𝑠) − 1)) · -1)) |
| 92 | 24, 11 | mulcomd 11282 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((-1↑((♯‘𝑠) − 1)) · -1) = (-1 ·
(-1↑((♯‘𝑠)
− 1)))) |
| 93 | 24 | mulm1d 11715 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1
· (-1↑((♯‘𝑠) − 1))) =
-(-1↑((♯‘𝑠) − 1))) |
| 94 | 91, 92, 93 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-1↑(♯‘𝑠))
= -(-1↑((♯‘𝑠) − 1))) |
| 95 | 25 | unissd 4917 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∪ 𝑠 ⊆ ∪ 𝐴) |
| 96 | 31, 95 | sstrd 3994 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∩ 𝑠 ⊆ ∪ 𝐴) |
| 97 | | sseqin2 4223 |
. . . . . . . . . . 11
⊢ (∩ 𝑠
⊆ ∪ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑠) =
∩ 𝑠) |
| 98 | 96, 97 | sylib 218 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(∪ 𝐴 ∩ ∩ 𝑠) = ∩
𝑠) |
| 99 | 98 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∩ 𝑠)) |
| 100 | 94, 99 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))) = (-(-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠))) |
| 101 | 24, 35 | mulneg1d 11716 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))
= -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) |
| 102 | 100, 101 | eqtr2d 2778 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))
= ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠)))) |
| 103 | 102 | sumeq2dv 15738 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))
= Σ𝑠 ∈
(𝒫 𝐴 ∖
{∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠)))) |
| 104 | 89, 103 | eqtr3d 2779 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
-Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))
= Σ𝑠 ∈
(𝒫 𝐴 ∖
{∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠)))) |
| 105 | 88, 104 | oveq12d 7449 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
= (Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))))) |
| 106 | 70, 105 | eqtr3d 2779 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
= (Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴
∩ ∩ 𝑠))))) |
| 107 | 61, 69, 106 | 3eqtr4rd 2788 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
= 0) |
| 108 | 4, 37, 107 | subeq0d 11628 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(♯‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) |