Metamath Proof Explorer


Theorem incexc2

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

Ref Expression
Assertion incexc2 ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ( ( - 1 ↑ ( 𝑛 − 1 ) ) · Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ♯ ‘ 𝑠 ) ) )

Proof

Step Hyp Ref Expression
1 incexc ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ 𝐴 ) = Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) )
2 hashcl ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
3 2 ad2antrr ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
4 3 nn0zd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
5 simpl ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 𝐴 ∈ Fin )
6 elpwi ( 𝑘 ∈ 𝒫 𝐴𝑘𝐴 )
7 ssdomg ( 𝐴 ∈ Fin → ( 𝑘𝐴𝑘𝐴 ) )
8 7 imp ( ( 𝐴 ∈ Fin ∧ 𝑘𝐴 ) → 𝑘𝐴 )
9 5 6 8 syl2an ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → 𝑘𝐴 )
10 hashdomi ( 𝑘𝐴 → ( ♯ ‘ 𝑘 ) ≤ ( ♯ ‘ 𝐴 ) )
11 9 10 syl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → ( ♯ ‘ 𝑘 ) ≤ ( ♯ ‘ 𝐴 ) )
12 fznn ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( ( ♯ ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( ( ♯ ‘ 𝑘 ) ∈ ℕ ∧ ( ♯ ‘ 𝑘 ) ≤ ( ♯ ‘ 𝐴 ) ) ) )
13 12 rbaibd ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝑘 ) ≤ ( ♯ ‘ 𝐴 ) ) → ( ( ♯ ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( ♯ ‘ 𝑘 ) ∈ ℕ ) )
14 4 11 13 syl2anc ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → ( ( ♯ ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( ♯ ‘ 𝑘 ) ∈ ℕ ) )
15 ssfi ( ( 𝐴 ∈ Fin ∧ 𝑘𝐴 ) → 𝑘 ∈ Fin )
16 5 6 15 syl2an ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → 𝑘 ∈ Fin )
17 hashnncl ( 𝑘 ∈ Fin → ( ( ♯ ‘ 𝑘 ) ∈ ℕ ↔ 𝑘 ≠ ∅ ) )
18 16 17 syl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → ( ( ♯ ‘ 𝑘 ) ∈ ℕ ↔ 𝑘 ≠ ∅ ) )
19 14 18 bitr2d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → ( 𝑘 ≠ ∅ ↔ ( ♯ ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
20 df-ne ( 𝑘 ≠ ∅ ↔ ¬ 𝑘 = ∅ )
21 risset ( ( ♯ ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ∃ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) 𝑛 = ( ♯ ‘ 𝑘 ) )
22 19 20 21 3bitr3g ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → ( ¬ 𝑘 = ∅ ↔ ∃ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) 𝑛 = ( ♯ ‘ 𝑘 ) ) )
23 velsn ( 𝑘 ∈ { ∅ } ↔ 𝑘 = ∅ )
24 23 notbii ( ¬ 𝑘 ∈ { ∅ } ↔ ¬ 𝑘 = ∅ )
25 eqcom ( ( ♯ ‘ 𝑘 ) = 𝑛𝑛 = ( ♯ ‘ 𝑘 ) )
26 25 rexbii ( ∃ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ( ♯ ‘ 𝑘 ) = 𝑛 ↔ ∃ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) 𝑛 = ( ♯ ‘ 𝑘 ) )
27 22 24 26 3bitr4g ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑘 ∈ 𝒫 𝐴 ) → ( ¬ 𝑘 ∈ { ∅ } ↔ ∃ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ( ♯ ‘ 𝑘 ) = 𝑛 ) )
28 27 rabbidva ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → { 𝑘 ∈ 𝒫 𝐴 ∣ ¬ 𝑘 ∈ { ∅ } } = { 𝑘 ∈ 𝒫 𝐴 ∣ ∃ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ( ♯ ‘ 𝑘 ) = 𝑛 } )
29 dfdif2 ( 𝒫 𝐴 ∖ { ∅ } ) = { 𝑘 ∈ 𝒫 𝐴 ∣ ¬ 𝑘 ∈ { ∅ } }
30 iunrab 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } = { 𝑘 ∈ 𝒫 𝐴 ∣ ∃ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ( ♯ ‘ 𝑘 ) = 𝑛 }
31 28 29 30 3eqtr4g ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( 𝒫 𝐴 ∖ { ∅ } ) = 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } )
32 31 sumeq1d ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) = Σ 𝑠 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) )
33 1 32 eqtrd ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ 𝐴 ) = Σ 𝑠 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) )
34 fzfid ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin )
35 simpll ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝐴 ∈ Fin )
36 pwfi ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
37 35 36 sylib ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝒫 𝐴 ∈ Fin )
38 ssrab2 { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ⊆ 𝒫 𝐴
39 ssfi ( ( 𝒫 𝐴 ∈ Fin ∧ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ⊆ 𝒫 𝐴 ) → { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ∈ Fin )
40 37 38 39 sylancl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ∈ Fin )
41 fveqeq2 ( 𝑘 = 𝑠 → ( ( ♯ ‘ 𝑘 ) = 𝑛 ↔ ( ♯ ‘ 𝑠 ) = 𝑛 ) )
42 41 elrab ( 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ↔ ( 𝑠 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑠 ) = 𝑛 ) )
43 42 simprbi ( 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } → ( ♯ ‘ 𝑠 ) = 𝑛 )
44 43 adantl ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( ♯ ‘ 𝑠 ) = 𝑛 )
45 44 ralrimiva ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ∀ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ♯ ‘ 𝑠 ) = 𝑛 )
46 45 ralrimiva ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ∀ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∀ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ♯ ‘ 𝑠 ) = 𝑛 )
47 invdisj ( ∀ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∀ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ♯ ‘ 𝑠 ) = 𝑛Disj 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } )
48 46 47 syl ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Disj 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } )
49 44 oveq1d ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( ( ♯ ‘ 𝑠 ) − 1 ) = ( 𝑛 − 1 ) )
50 49 oveq2d ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) = ( - 1 ↑ ( 𝑛 − 1 ) ) )
51 50 oveq1d ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) = ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ♯ ‘ 𝑠 ) ) )
52 1cnd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 1 ∈ ℂ )
53 52 negcld ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → - 1 ∈ ℂ )
54 elfznn ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
55 54 adantl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
56 nnm1nn0 ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
57 55 56 syl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑛 − 1 ) ∈ ℕ0 )
58 53 57 expcld ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( - 1 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
59 58 adantr ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( - 1 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
60 unifi ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 𝐴 ∈ Fin )
61 60 ad2antrr ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝐴 ∈ Fin )
62 55 adantr ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝑛 ∈ ℕ )
63 44 62 eqeltrd ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( ♯ ‘ 𝑠 ) ∈ ℕ )
64 35 adantr ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝐴 ∈ Fin )
65 elrabi ( 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } → 𝑠 ∈ 𝒫 𝐴 )
66 65 adantl ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝑠 ∈ 𝒫 𝐴 )
67 elpwi ( 𝑠 ∈ 𝒫 𝐴𝑠𝐴 )
68 66 67 syl ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝑠𝐴 )
69 64 68 ssfid ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝑠 ∈ Fin )
70 hashnncl ( 𝑠 ∈ Fin → ( ( ♯ ‘ 𝑠 ) ∈ ℕ ↔ 𝑠 ≠ ∅ ) )
71 69 70 syl ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( ( ♯ ‘ 𝑠 ) ∈ ℕ ↔ 𝑠 ≠ ∅ ) )
72 63 71 mpbid ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝑠 ≠ ∅ )
73 intssuni ( 𝑠 ≠ ∅ → 𝑠 𝑠 )
74 72 73 syl ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝑠 𝑠 )
75 68 unissd ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝑠 𝐴 )
76 74 75 sstrd ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝑠 𝐴 )
77 61 76 ssfid ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → 𝑠 ∈ Fin )
78 hashcl ( 𝑠 ∈ Fin → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
79 77 78 syl ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
80 79 nn0cnd ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( ♯ ‘ 𝑠 ) ∈ ℂ )
81 59 80 mulcld ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ♯ ‘ 𝑠 ) ) ∈ ℂ )
82 51 81 eqeltrd ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) → ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) ∈ ℂ )
83 82 anasss ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ) ) → ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) ∈ ℂ )
84 34 40 48 83 fsumiun ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ 𝑠 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) = Σ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) )
85 51 sumeq2dv ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) = Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ♯ ‘ 𝑠 ) ) )
86 40 58 80 fsummulc2 ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( - 1 ↑ ( 𝑛 − 1 ) ) · Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ♯ ‘ 𝑠 ) ) = Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ♯ ‘ 𝑠 ) ) )
87 85 86 eqtr4d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) = ( ( - 1 ↑ ( 𝑛 − 1 ) ) · Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ♯ ‘ 𝑠 ) ) )
88 87 sumeq2dv ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ 𝑠 ) ) = Σ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ( ( - 1 ↑ ( 𝑛 − 1 ) ) · Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ♯ ‘ 𝑠 ) ) )
89 33 84 88 3eqtrd ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ( ( - 1 ↑ ( 𝑛 − 1 ) ) · Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ♯ ‘ 𝑠 ) ) )