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 ) ) · Σ 𝑠 ∈ { 𝑘 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑘 ) = 𝑛 } ( ♯ ‘ ∩ 𝑠 ) ) )