Metamath Proof Explorer

Theorem incexc

Description: The inclusion/exclusion principle for counting the elements of a finite union of finite sets. This is Metamath 100 proof #96. (Contributed by Mario Carneiro, 7-Aug-2017)

Ref Expression
Assertion incexc ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) )

Proof

Step Hyp Ref Expression
1 unifi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ∪ 𝐴 ∈ Fin )
2 hashcl ⊢ ( ∪ 𝐴 ∈ Fin → ( ♯ ‘ ∪ 𝐴 ) ∈ ℕ0 )
3 2 nn0cnd ⊢ ( ∪ 𝐴 ∈ Fin → ( ♯ ‘ ∪ 𝐴 ) ∈ ℂ )
4 1 3 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) ∈ ℂ )
5 simpl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 𝐴 ∈ Fin )
6 pwfi ⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
7 5 6 sylib ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 𝒫 𝐴 ∈ Fin )
8 diffi ⊢ ( 𝒫 𝐴 ∈ Fin → ( 𝒫 𝐴 ∖ { ∅ } ) ∈ Fin )
9 7 8 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( 𝒫 𝐴 ∖ { ∅ } ) ∈ Fin )
10 1cnd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → 1 ∈ ℂ )
11 10 negcld ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → - 1 ∈ ℂ )
12 eldifsni ⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝑠 ≠ ∅ )
13 12 adantl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → 𝑠 ≠ ∅ )
14 eldifi ⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝑠 ∈ 𝒫 𝐴 )
15 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴 )
16 14 15 syl ⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝑠 ⊆ 𝐴 )
17 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴 ) → 𝑠 ∈ Fin )
18 5 16 17 syl2an ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → 𝑠 ∈ Fin )
19 hashnncl ⊢ ( 𝑠 ∈ Fin → ( ( ♯ ‘ 𝑠 ) ∈ ℕ ↔ 𝑠 ≠ ∅ ) )
20 18 19 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ( ♯ ‘ 𝑠 ) ∈ ℕ ↔ 𝑠 ≠ ∅ ) )
21 13 20 mpbird ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ♯ ‘ 𝑠 ) ∈ ℕ )
22 nnm1nn0 ⊢ ( ( ♯ ‘ 𝑠 ) ∈ ℕ → ( ( ♯ ‘ 𝑠 ) − 1 ) ∈ ℕ0 )
23 21 22 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ( ♯ ‘ 𝑠 ) − 1 ) ∈ ℕ0 )
24 11 23 expcld ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) ∈ ℂ )
25 16 adantl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → 𝑠 ⊆ 𝐴 )
26 simplr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → 𝐴 ⊆ Fin )
27 25 26 sstrd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → 𝑠 ⊆ Fin )
28 unifi ⊢ ( ( 𝑠 ∈ Fin ∧ 𝑠 ⊆ Fin ) → ∪ 𝑠 ∈ Fin )
29 18 27 28 syl2anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∪ 𝑠 ∈ Fin )
30 intssuni ⊢ ( 𝑠 ≠ ∅ → ∩ 𝑠 ⊆ ∪ 𝑠 )
31 13 30 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∩ 𝑠 ⊆ ∪ 𝑠 )
32 29 31 ssfid ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∩ 𝑠 ∈ Fin )
33 hashcl ⊢ ( ∩ 𝑠 ∈ Fin → ( ♯ ‘ ∩ 𝑠 ) ∈ ℕ0 )
34 32 33 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ♯ ‘ ∩ 𝑠 ) ∈ ℕ0 )
35 34 nn0cnd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ♯ ‘ ∩ 𝑠 ) ∈ ℂ )
36 24 35 mulcld ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) ∈ ℂ )
37 9 36 fsumcl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) ∈ ℂ )
38 disjdif ⊢ ( { ∅ } ∩ ( 𝒫 𝐴 ∖ { ∅ } ) ) = ∅
39 38 a1i ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( { ∅ } ∩ ( 𝒫 𝐴 ∖ { ∅ } ) ) = ∅ )
40 0elpw ⊢ ∅ ∈ 𝒫 𝐴
41 snssi ⊢ ( ∅ ∈ 𝒫 𝐴 → { ∅ } ⊆ 𝒫 𝐴 )
42 40 41 ax-mp ⊢ { ∅ } ⊆ 𝒫 𝐴
43 undif ⊢ ( { ∅ } ⊆ 𝒫 𝐴 ↔ ( { ∅ } ∪ ( 𝒫 𝐴 ∖ { ∅ } ) ) = 𝒫 𝐴 )
44 42 43 mpbi ⊢ ( { ∅ } ∪ ( 𝒫 𝐴 ∖ { ∅ } ) ) = 𝒫 𝐴
45 44 eqcomi ⊢ 𝒫 𝐴 = ( { ∅ } ∪ ( 𝒫 𝐴 ∖ { ∅ } ) )
46 45 a1i ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 𝒫 𝐴 = ( { ∅ } ∪ ( 𝒫 𝐴 ∖ { ∅ } ) ) )
47 1cnd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → 1 ∈ ℂ )
48 47 negcld ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → - 1 ∈ ℂ )
49 5 15 17 syl2an ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → 𝑠 ∈ Fin )
50 hashcl ⊢ ( 𝑠 ∈ Fin → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
51 49 50 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
52 48 51 expcld ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) ∈ ℂ )
53 1 adantr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → ∪ 𝐴 ∈ Fin )
54 inss1 ⊢ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ⊆ ∪ 𝐴
55 ssfi ⊢ ( ( ∪ 𝐴 ∈ Fin ∧ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ⊆ ∪ 𝐴 ) → ( ∪ 𝐴 ∩ ∩ 𝑠 ) ∈ Fin )
56 53 54 55 sylancl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → ( ∪ 𝐴 ∩ ∩ 𝑠 ) ∈ Fin )
57 hashcl ⊢ ( ( ∪ 𝐴 ∩ ∩ 𝑠 ) ∈ Fin → ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ∈ ℕ0 )
58 56 57 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ∈ ℕ0 )
59 58 nn0cnd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ∈ ℂ )
60 52 59 mulcld ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ 𝒫 𝐴 ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) ∈ ℂ )
61 39 46 7 60 fsumsplit ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) = ( Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) + Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) ) )
62 inidm ⊢ ( ∪ 𝐴 ∩ ∪ 𝐴 ) = ∪ 𝐴
63 62 fveq2i ⊢ ( ♯ ‘ ( ∪ 𝐴 ∩ ∪ 𝐴 ) ) = ( ♯ ‘ ∪ 𝐴 )
64 63 oveq2i ⊢ ( ( ♯ ‘ ∪ 𝐴 ) − ( ♯ ‘ ( ∪ 𝐴 ∩ ∪ 𝐴 ) ) ) = ( ( ♯ ‘ ∪ 𝐴 ) − ( ♯ ‘ ∪ 𝐴 ) )
65 4 subidd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ( ♯ ‘ ∪ 𝐴 ) − ( ♯ ‘ ∪ 𝐴 ) ) = 0 )
66 64 65 eqtrid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ( ♯ ‘ ∪ 𝐴 ) − ( ♯ ‘ ( ∪ 𝐴 ∩ ∪ 𝐴 ) ) ) = 0 )
67 incexclem ⊢ ( ( 𝐴 ∈ Fin ∧ ∪ 𝐴 ∈ Fin ) → ( ( ♯ ‘ ∪ 𝐴 ) − ( ♯ ‘ ( ∪ 𝐴 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) )
68 1 67 syldan ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ( ♯ ‘ ∪ 𝐴 ) − ( ♯ ‘ ( ∪ 𝐴 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) )
69 66 68 eqtr3d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 0 = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) )
70 4 37 negsubd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ( ♯ ‘ ∪ 𝐴 ) + - Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) ) = ( ( ♯ ‘ ∪ 𝐴 ) − Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) ) )
71 0ex ⊢ ∅ ∈ V
72 1cnd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 1 ∈ ℂ )
73 72 4 mulcld ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( 1 · ( ♯ ‘ ∪ 𝐴 ) ) ∈ ℂ )
74 fveq2 ⊢ ( 𝑠 = ∅ → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ∅ ) )
75 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
76 74 75 eqtrdi ⊢ ( 𝑠 = ∅ → ( ♯ ‘ 𝑠 ) = 0 )
77 76 oveq2d ⊢ ( 𝑠 = ∅ → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = ( - 1 ↑ 0 ) )
78 neg1cn ⊢ - 1 ∈ ℂ
79 exp0 ⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
80 78 79 ax-mp ⊢ ( - 1 ↑ 0 ) = 1
81 77 80 eqtrdi ⊢ ( 𝑠 = ∅ → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = 1 )
82 rint0 ⊢ ( 𝑠 = ∅ → ( ∪ 𝐴 ∩ ∩ 𝑠 ) = ∪ 𝐴 )
83 82 fveq2d ⊢ ( 𝑠 = ∅ → ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ∪ 𝐴 ) )
84 81 83 oveq12d ⊢ ( 𝑠 = ∅ → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) = ( 1 · ( ♯ ‘ ∪ 𝐴 ) ) )
85 84 sumsn ⊢ ( ( ∅ ∈ V ∧ ( 1 · ( ♯ ‘ ∪ 𝐴 ) ) ∈ ℂ ) → Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) = ( 1 · ( ♯ ‘ ∪ 𝐴 ) ) )
86 71 73 85 sylancr ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) = ( 1 · ( ♯ ‘ ∪ 𝐴 ) ) )
87 4 mullidd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( 1 · ( ♯ ‘ ∪ 𝐴 ) ) = ( ♯ ‘ ∪ 𝐴 ) )
88 86 87 eqtr2d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) )
89 9 36 fsumneg ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) - ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) = - Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) )
90 expm1t ⊢ ( ( - 1 ∈ ℂ ∧ ( ♯ ‘ 𝑠 ) ∈ ℕ ) → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · - 1 ) )
91 11 21 90 syl2anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · - 1 ) )
92 24 11 mulcomd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · - 1 ) = ( - 1 · ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) ) )
93 24 mulm1d ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( - 1 · ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) ) = - ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) )
94 91 92 93 3eqtrd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = - ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) )
95 25 unissd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∪ 𝑠 ⊆ ∪ 𝐴 )
96 31 95 sstrd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∩ 𝑠 ⊆ ∪ 𝐴 )
97 sseqin2 ⊢ ( ∩ 𝑠 ⊆ ∪ 𝐴 ↔ ( ∪ 𝐴 ∩ ∩ 𝑠 ) = ∩ 𝑠 )
98 96 97 sylib ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ∪ 𝐴 ∩ ∩ 𝑠 ) = ∩ 𝑠 )
99 98 fveq2d ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ∩ 𝑠 ) )
100 94 99 oveq12d ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) = ( - ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) )
101 24 35 mulneg1d ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( - ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) = - ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) )
102 100 101 eqtr2d ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → - ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) )
103 102 sumeq2dv ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) - ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) = Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) )
104 89 103 eqtr3d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → - Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) = Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) )
105 88 104 oveq12d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ( ♯ ‘ ∪ 𝐴 ) + - Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) ) = ( Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) + Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) ) )
106 70 105 eqtr3d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ( ♯ ‘ ∪ 𝐴 ) − Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) ) = ( Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) + Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( ∪ 𝐴 ∩ ∩ 𝑠 ) ) ) ) )
107 61 69 106 3eqtr4rd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ( ♯ ‘ ∪ 𝐴 ) − Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) ) = 0 )
108 4 37 107 subeq0d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) )