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 A Fin A Fin A = s 𝒫 A 1 s 1 s

Proof

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