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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ 𝑠 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) − 1 ) ) · ( ♯ ‘ ∩ 𝑠 ) ) )

Proof

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