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