incexc - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > incexc		Structured version Visualization version GIF version

Theorem incexc 15744

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.)

**Assertion**
Ref	Expression
incexc	⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))

Distinct variable group: 𝐴,𝑠

**Proof of Theorem incexc**
Step	Hyp	Ref	Expression
1		unifi 9228	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴 ∈ Fin)
2		hashcl 14263	. . . 4 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℕ₀)
3	2	nn0cnd 12444	. . 3 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℂ)
4	1, 3	syl 17	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) ∈ ℂ)
5		simpl 482	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
6		pwfi 9203	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
7	5, 6	sylib 218	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 ∈ Fin)
8		diffi 9084	. . . 4 ⊢ (𝒫 𝐴 ∈ Fin → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
9	7, 8	syl 17	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
10		1cnd 11107	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 1 ∈ ℂ)
11	10	negcld 11459	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -1 ∈ ℂ)
12		eldifsni 4739	. . . . . . . 8 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ≠ ∅)
13	12	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ≠ ∅)
14		eldifi 4078	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ∈ 𝒫 𝐴)
15		elpwi 4554	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ⊆ 𝐴)
17		ssfi 9082	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin)
18	5, 16, 17	syl2an 596	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ∈ Fin)
19		hashnncl 14273	. . . . . . . 8 ⊢ (𝑠 ∈ Fin → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
20	18, 19	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
21	13, 20	mpbird 257	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘𝑠) ∈ ℕ)
22		nnm1nn0 12422	. . . . . 6 ⊢ ((♯‘𝑠) ∈ ℕ → ((♯‘𝑠) − 1) ∈ ℕ₀)
23	21, 22	syl 17	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) − 1) ∈ ℕ₀)
24	11, 23	expcld 14053	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑((♯‘𝑠) − 1)) ∈ ℂ)
25	16	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ 𝐴)
26		simplr 768	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝐴 ⊆ Fin)
27	25, 26	sstrd 3940	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ Fin)
28		unifi 9228	. . . . . . . 8 ⊢ ((𝑠 ∈ Fin ∧ 𝑠 ⊆ Fin) → ∪ 𝑠 ∈ Fin)
29	18, 27, 28	syl2anc 584	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ∈ Fin)
30		intssuni 4918	. . . . . . . 8 ⊢ (𝑠 ≠ ∅ → ∩ 𝑠 ⊆ ∪ 𝑠)
31	13, 30	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝑠)
32	29, 31	ssfid 9153	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ∈ Fin)
33		hashcl 14263	. . . . . 6 ⊢ (∩ 𝑠 ∈ Fin → (♯‘∩ 𝑠) ∈ ℕ₀)
34	32, 33	syl 17	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℕ₀)
35	34	nn0cnd 12444	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℂ)
36	24, 35	mulcld 11132	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
37	9, 36	fsumcl 15640	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
38		disjdif 4419	. . . . 5 ⊢ ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅
39	38	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅)
40		0elpw 5292	. . . . . . . 8 ⊢ ∅ ∈ 𝒫 𝐴
41		snssi 4757	. . . . . . . 8 ⊢ (∅ ∈ 𝒫 𝐴 → {∅} ⊆ 𝒫 𝐴)
42	40, 41	ax-mp 5	. . . . . . 7 ⊢ {∅} ⊆ 𝒫 𝐴
43		undif 4429	. . . . . . 7 ⊢ ({∅} ⊆ 𝒫 𝐴 ↔ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴)
44	42, 43	mpbi 230	. . . . . 6 ⊢ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴
45	44	eqcomi 2740	. . . . 5 ⊢ 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅}))
46	45	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅})))
47		1cnd 11107	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 1 ∈ ℂ)
48	47	negcld 11459	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → -1 ∈ ℂ)
49	5, 15, 17	syl2an 596	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑠 ∈ Fin)
50		hashcl 14263	. . . . . . 7 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
51	49, 50	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘𝑠) ∈ ℕ₀)
52	48, 51	expcld 14053	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (-1↑(♯‘𝑠)) ∈ ℂ)
53	1	adantr 480	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ∪ 𝐴 ∈ Fin)
54		inss1 4184	. . . . . . . 8 ⊢ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴
55		ssfi 9082	. . . . . . . 8 ⊢ ((∪ 𝐴 ∈ Fin ∧ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
56	53, 54, 55	sylancl 586	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
57		hashcl 14263	. . . . . . 7 ⊢ ((∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
58	56, 57	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
59	58	nn0cnd 12444	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℂ)
60	52, 59	mulcld 11132	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) ∈ ℂ)
61	39, 46, 7, 60	fsumsplit 15648	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
62		inidm 4174	. . . . . . 7 ⊢ (∪ 𝐴 ∩ ∪ 𝐴) = ∪ 𝐴
63	62	fveq2i 6825	. . . . . 6 ⊢ (♯‘(∪ 𝐴 ∩ ∪ 𝐴)) = (♯‘∪ 𝐴)
64	63	oveq2i 7357	. . . . 5 ⊢ ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = ((♯‘∪ 𝐴) − (♯‘∪ 𝐴))
65	4	subidd 11460	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘∪ 𝐴)) = 0)
66	64, 65	eqtrid 2778	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = 0)
67		incexclem 15743	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ ∪ 𝐴 ∈ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
68	1, 67	syldan 591	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
69	66, 68	eqtr3d 2768	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 0 = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
70	4, 37	negsubd 11478	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))))
71		0ex 5243	. . . . . . 7 ⊢ ∅ ∈ V
72		1cnd 11107	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 1 ∈ ℂ)
73	72, 4	mulcld 11132	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) ∈ ℂ)
74		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑠 = ∅ → (♯‘𝑠) = (♯‘∅))
75		hash0 14274	. . . . . . . . . . . 12 ⊢ (♯‘∅) = 0
76	74, 75	eqtrdi 2782	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (♯‘𝑠) = 0)
77	76	oveq2d 7362	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = (-1↑0))
78		neg1cn 12110	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
79		exp0 13972	. . . . . . . . . . 11 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
80	78, 79	ax-mp 5	. . . . . . . . . 10 ⊢ (-1↑0) = 1
81	77, 80	eqtrdi 2782	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = 1)
82		rint0 4936	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (∪ 𝐴 ∩ ∩ 𝑠) = ∪ 𝐴)
83	82	fveq2d 6826	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∪ 𝐴))
84	81, 83	oveq12d 7364	. . . . . . . 8 ⊢ (𝑠 = ∅ → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
85	84	sumsn 15653	. . . . . . 7 ⊢ ((∅ ∈ V ∧ (1 · (♯‘∪ 𝐴)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
86	71, 73, 85	sylancr 587	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
87	4	mullidd 11130	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) = (♯‘∪ 𝐴))
88	86, 87	eqtr2d 2767	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
89	9, 36	fsumneg 15694	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
90		expm1t 13997	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ (♯‘𝑠) ∈ ℕ) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
91	11, 21, 90	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
92	24, 11	mulcomd 11133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · -1) = (-1 · (-1↑((♯‘𝑠) − 1))))
93	24	mulm1d 11569	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1 · (-1↑((♯‘𝑠) − 1))) = -(-1↑((♯‘𝑠) − 1)))
94	91, 92, 93	3eqtrd 2770	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = -(-1↑((♯‘𝑠) − 1)))
95	25	unissd 4866	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ⊆ ∪ 𝐴)
96	31, 95	sstrd 3940	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝐴)
97		sseqin2 4170	. . . . . . . . . . 11 ⊢ (∩ 𝑠 ⊆ ∪ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
98	96, 97	sylib 218	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
99	98	fveq2d 6826	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∩ 𝑠))
100	94, 99	oveq12d 7364	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
101	24, 35	mulneg1d 11570	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
102	100, 101	eqtr2d 2767	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
103	102	sumeq2dv 15609	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
104	89, 103	eqtr3d 2768	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
105	88, 104	oveq12d 7364	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
106	70, 105	eqtr3d 2768	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
107	61, 69, 106	3eqtr4rd 2777	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = 0)
108	4, 37, 107	subeq0d 11480	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 Vcvv 3436 ∖ cdif 3894 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 ∅c0 4280 𝒫 cpw 4547 {csn 4573 ∪ cuni 4856 ∩ cint 4895 ‘cfv 6481 (class class class)co 7346 Fincfn 8869 ℂcc 11004 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 − cmin 11344 -cneg 11345 ℕcn 12125 ℕ₀cn0 12381 ↑cexp 13968 ♯chash 14237 Σcsu 15593

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-oadd 8389 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-oi 9396 df-dju 9794 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-rp 12891 df-fz 13408 df-fzo 13555 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-sum 15594

This theorem is referenced by: incexc2 15745

W3C validator