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 
|- ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ n e. ( 1 ... ( # ` A ) ) ( ( -u 1 ^ ( n - 1 ) ) x. sum_ s e. { k e. ~P A | ( # ` k ) = n } ( # ` |^| s ) ) )

Proof

Step Hyp Ref Expression
1 incexc 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )
2 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
3 2 ad2antrr 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> ( # ` A ) e. NN0 )
4 3 nn0zd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> ( # ` A ) e. ZZ )
5 simpl 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> A e. Fin )
6 elpwi 
 |-  ( k e. ~P A -> k C_ A )
7 ssdomg 
 |-  ( A e. Fin -> ( k C_ A -> k ~<_ A ) )
8 7 imp 
 |-  ( ( A e. Fin /\ k C_ A ) -> k ~<_ A )
9 5 6 8 syl2an 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> k ~<_ A )
10 hashdomi 
 |-  ( k ~<_ A -> ( # ` k ) <_ ( # ` A ) )
11 9 10 syl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> ( # ` k ) <_ ( # ` A ) )
12 fznn 
 |-  ( ( # ` A ) e. ZZ -> ( ( # ` k ) e. ( 1 ... ( # ` A ) ) <-> ( ( # ` k ) e. NN /\ ( # ` k ) <_ ( # ` A ) ) ) )
13 12 rbaibd 
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` k ) <_ ( # ` A ) ) -> ( ( # ` k ) e. ( 1 ... ( # ` A ) ) <-> ( # ` k ) e. NN ) )
14 4 11 13 syl2anc 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> ( ( # ` k ) e. ( 1 ... ( # ` A ) ) <-> ( # ` k ) e. NN ) )
15 ssfi 
 |-  ( ( A e. Fin /\ k C_ A ) -> k e. Fin )
16 5 6 15 syl2an 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> k e. Fin )
17 hashnncl 
 |-  ( k e. Fin -> ( ( # ` k ) e. NN <-> k =/= (/) ) )
18 16 17 syl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> ( ( # ` k ) e. NN <-> k =/= (/) ) )
19 14 18 bitr2d 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> ( k =/= (/) <-> ( # ` k ) e. ( 1 ... ( # ` A ) ) ) )
20 df-ne 
 |-  ( k =/= (/) <-> -. k = (/) )
21 risset 
 |-  ( ( # ` k ) e. ( 1 ... ( # ` A ) ) <-> E. n e. ( 1 ... ( # ` A ) ) n = ( # ` k ) )
22 19 20 21 3bitr3g 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> ( -. k = (/) <-> E. n e. ( 1 ... ( # ` A ) ) n = ( # ` k ) ) )
23 velsn 
 |-  ( k e. { (/) } <-> k = (/) )
24 23 notbii 
 |-  ( -. k e. { (/) } <-> -. k = (/) )
25 eqcom 
 |-  ( ( # ` k ) = n <-> n = ( # ` k ) )
26 25 rexbii 
 |-  ( E. n e. ( 1 ... ( # ` A ) ) ( # ` k ) = n <-> E. n e. ( 1 ... ( # ` A ) ) n = ( # ` k ) )
27 22 24 26 3bitr4g 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ k e. ~P A ) -> ( -. k e. { (/) } <-> E. n e. ( 1 ... ( # ` A ) ) ( # ` k ) = n ) )
28 27 rabbidva 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> { k e. ~P A | -. k e. { (/) } } = { k e. ~P A | E. n e. ( 1 ... ( # ` A ) ) ( # ` k ) = n } )
29 dfdif2 
 |-  ( ~P A \ { (/) } ) = { k e. ~P A | -. k e. { (/) } }
30 iunrab 
 |-  U_ n e. ( 1 ... ( # ` A ) ) { k e. ~P A | ( # ` k ) = n } = { k e. ~P A | E. n e. ( 1 ... ( # ` A ) ) ( # ` k ) = n }
31 28 29 30 3eqtr4g 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( ~P A \ { (/) } ) = U_ n e. ( 1 ... ( # ` A ) ) { k e. ~P A | ( # ` k ) = n } )
32 31 sumeq1d 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = sum_ s e. U_ n e. ( 1 ... ( # ` A ) ) { k e. ~P A | ( # ` k ) = n } ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )
33 1 32 eqtrd 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ s e. U_ n e. ( 1 ... ( # ` A ) ) { k e. ~P A | ( # ` k ) = n } ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )
34 fzfid 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( 1 ... ( # ` A ) ) e. Fin )
35 simpll 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> A e. Fin )
36 pwfi 
 |-  ( A e. Fin <-> ~P A e. Fin )
37 35 36 sylib 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ~P A e. Fin )
38 ssrab2 
 |-  { k e. ~P A | ( # ` k ) = n } C_ ~P A
39 ssfi 
 |-  ( ( ~P A e. Fin /\ { k e. ~P A | ( # ` k ) = n } C_ ~P A ) -> { k e. ~P A | ( # ` k ) = n } e. Fin )
40 37 38 39 sylancl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> { k e. ~P A | ( # ` k ) = n } e. Fin )
41 fveqeq2 
 |-  ( k = s -> ( ( # ` k ) = n <-> ( # ` s ) = n ) )
42 41 elrab 
 |-  ( s e. { k e. ~P A | ( # ` k ) = n } <-> ( s e. ~P A /\ ( # ` s ) = n ) )
43 42 simprbi 
 |-  ( s e. { k e. ~P A | ( # ` k ) = n } -> ( # ` s ) = n )
44 43 adantl 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( # ` s ) = n )
45 44 ralrimiva 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> A. s e. { k e. ~P A | ( # ` k ) = n } ( # ` s ) = n )
46 45 ralrimiva 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> A. n e. ( 1 ... ( # ` A ) ) A. s e. { k e. ~P A | ( # ` k ) = n } ( # ` s ) = n )
47 invdisj 
 |-  ( A. n e. ( 1 ... ( # ` A ) ) A. s e. { k e. ~P A | ( # ` k ) = n } ( # ` s ) = n -> Disj_ n e. ( 1 ... ( # ` A ) ) { k e. ~P A | ( # ` k ) = n } )
48 46 47 syl 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> Disj_ n e. ( 1 ... ( # ` A ) ) { k e. ~P A | ( # ` k ) = n } )
49 44 oveq1d 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( ( # ` s ) - 1 ) = ( n - 1 ) )
50 49 oveq2d 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( -u 1 ^ ( ( # ` s ) - 1 ) ) = ( -u 1 ^ ( n - 1 ) ) )
51 50 oveq1d 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = ( ( -u 1 ^ ( n - 1 ) ) x. ( # ` |^| s ) ) )
52 1cnd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> 1 e. CC )
53 52 negcld 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> -u 1 e. CC )
54 elfznn 
 |-  ( n e. ( 1 ... ( # ` A ) ) -> n e. NN )
55 54 adantl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> n e. NN )
56 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
57 55 56 syl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( n - 1 ) e. NN0 )
58 53 57 expcld 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( -u 1 ^ ( n - 1 ) ) e. CC )
59 58 adantr 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( -u 1 ^ ( n - 1 ) ) e. CC )
60 unifi 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> U. A e. Fin )
61 60 ad2antrr 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> U. A e. Fin )
62 55 adantr 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> n e. NN )
63 44 62 eqeltrd 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( # ` s ) e. NN )
64 35 adantr 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> A e. Fin )
65 elrabi 
 |-  ( s e. { k e. ~P A | ( # ` k ) = n } -> s e. ~P A )
66 65 adantl 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> s e. ~P A )
67 elpwi 
 |-  ( s e. ~P A -> s C_ A )
68 66 67 syl 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> s C_ A )
69 64 68 ssfid 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> s e. Fin )
70 hashnncl 
 |-  ( s e. Fin -> ( ( # ` s ) e. NN <-> s =/= (/) ) )
71 69 70 syl 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( ( # ` s ) e. NN <-> s =/= (/) ) )
72 63 71 mpbid 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> s =/= (/) )
73 intssuni 
 |-  ( s =/= (/) -> |^| s C_ U. s )
74 72 73 syl 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> |^| s C_ U. s )
75 68 unissd 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> U. s C_ U. A )
76 74 75 sstrd 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> |^| s C_ U. A )
77 61 76 ssfid 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> |^| s e. Fin )
78 hashcl 
 |-  ( |^| s e. Fin -> ( # ` |^| s ) e. NN0 )
79 77 78 syl 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( # ` |^| s ) e. NN0 )
80 79 nn0cnd 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( # ` |^| s ) e. CC )
81 59 80 mulcld 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( ( -u 1 ^ ( n - 1 ) ) x. ( # ` |^| s ) ) e. CC )
82 51 81 eqeltrd 
 |-  ( ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) -> ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) e. CC )
83 82 anasss 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ ( n e. ( 1 ... ( # ` A ) ) /\ s e. { k e. ~P A | ( # ` k ) = n } ) ) -> ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) e. CC )
84 34 40 48 83 fsumiun 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> sum_ s e. U_ n e. ( 1 ... ( # ` A ) ) { k e. ~P A | ( # ` k ) = n } ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = sum_ n e. ( 1 ... ( # ` A ) ) sum_ s e. { k e. ~P A | ( # ` k ) = n } ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )
85 51 sumeq2dv 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> sum_ s e. { k e. ~P A | ( # ` k ) = n } ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = sum_ s e. { k e. ~P A | ( # ` k ) = n } ( ( -u 1 ^ ( n - 1 ) ) x. ( # ` |^| s ) ) )
86 40 58 80 fsummulc2 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( -u 1 ^ ( n - 1 ) ) x. sum_ s e. { k e. ~P A | ( # ` k ) = n } ( # ` |^| s ) ) = sum_ s e. { k e. ~P A | ( # ` k ) = n } ( ( -u 1 ^ ( n - 1 ) ) x. ( # ` |^| s ) ) )
87 85 86 eqtr4d 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ n e. ( 1 ... ( # ` A ) ) ) -> sum_ s e. { k e. ~P A | ( # ` k ) = n } ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = ( ( -u 1 ^ ( n - 1 ) ) x. sum_ s e. { k e. ~P A | ( # ` k ) = n } ( # ` |^| s ) ) )
88 87 sumeq2dv 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> sum_ n e. ( 1 ... ( # ` A ) ) sum_ s e. { k e. ~P A | ( # ` k ) = n } ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = sum_ n e. ( 1 ... ( # ` A ) ) ( ( -u 1 ^ ( n - 1 ) ) x. sum_ s e. { k e. ~P A | ( # ` k ) = n } ( # ` |^| s ) ) )
89 33 84 88 3eqtrd 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ n e. ( 1 ... ( # ` A ) ) ( ( -u 1 ^ ( n - 1 ) ) x. sum_ s e. { k e. ~P A | ( # ` k ) = n } ( # ` |^| s ) ) )