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 15780

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 9338	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴 ∈ Fin)
2		hashcl 14313	. . . 4 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℕ₀)
3	2	nn0cnd 12531	. . 3 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℂ)
4	1, 3	syl 17	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) ∈ ℂ)
5		simpl 484	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
6		pwfi 9175	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
7	5, 6	sylib 217	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 ∈ Fin)
8		diffi 9176	. . . 4 ⊢ (𝒫 𝐴 ∈ Fin → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
9	7, 8	syl 17	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
10		1cnd 11206	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 1 ∈ ℂ)
11	10	negcld 11555	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -1 ∈ ℂ)
12		eldifsni 4793	. . . . . . . 8 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ≠ ∅)
13	12	adantl 483	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ≠ ∅)
14		eldifi 4126	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ∈ 𝒫 𝐴)
15		elpwi 4609	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ⊆ 𝐴)
17		ssfi 9170	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin)
18	5, 16, 17	syl2an 597	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ∈ Fin)
19		hashnncl 14323	. . . . . . . 8 ⊢ (𝑠 ∈ Fin → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
20	18, 19	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
21	13, 20	mpbird 257	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘𝑠) ∈ ℕ)
22		nnm1nn0 12510	. . . . . 6 ⊢ ((♯‘𝑠) ∈ ℕ → ((♯‘𝑠) − 1) ∈ ℕ₀)
23	21, 22	syl 17	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) − 1) ∈ ℕ₀)
24	11, 23	expcld 14108	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑((♯‘𝑠) − 1)) ∈ ℂ)
25	16	adantl 483	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ 𝐴)
26		simplr 768	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝐴 ⊆ Fin)
27	25, 26	sstrd 3992	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ Fin)
28		unifi 9338	. . . . . . . 8 ⊢ ((𝑠 ∈ Fin ∧ 𝑠 ⊆ Fin) → ∪ 𝑠 ∈ Fin)
29	18, 27, 28	syl2anc 585	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ∈ Fin)
30		intssuni 4974	. . . . . . . 8 ⊢ (𝑠 ≠ ∅ → ∩ 𝑠 ⊆ ∪ 𝑠)
31	13, 30	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝑠)
32	29, 31	ssfid 9264	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ∈ Fin)
33		hashcl 14313	. . . . . 6 ⊢ (∩ 𝑠 ∈ Fin → (♯‘∩ 𝑠) ∈ ℕ₀)
34	32, 33	syl 17	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℕ₀)
35	34	nn0cnd 12531	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℂ)
36	24, 35	mulcld 11231	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
37	9, 36	fsumcl 15676	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
38		disjdif 4471	. . . . 5 ⊢ ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅
39	38	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅)
40		0elpw 5354	. . . . . . . 8 ⊢ ∅ ∈ 𝒫 𝐴
41		snssi 4811	. . . . . . . 8 ⊢ (∅ ∈ 𝒫 𝐴 → {∅} ⊆ 𝒫 𝐴)
42	40, 41	ax-mp 5	. . . . . . 7 ⊢ {∅} ⊆ 𝒫 𝐴
43		undif 4481	. . . . . . 7 ⊢ ({∅} ⊆ 𝒫 𝐴 ↔ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴)
44	42, 43	mpbi 229	. . . . . 6 ⊢ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴
45	44	eqcomi 2742	. . . . 5 ⊢ 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅}))
46	45	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅})))
47		1cnd 11206	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 1 ∈ ℂ)
48	47	negcld 11555	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → -1 ∈ ℂ)
49	5, 15, 17	syl2an 597	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑠 ∈ Fin)
50		hashcl 14313	. . . . . . 7 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
51	49, 50	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘𝑠) ∈ ℕ₀)
52	48, 51	expcld 14108	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (-1↑(♯‘𝑠)) ∈ ℂ)
53	1	adantr 482	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ∪ 𝐴 ∈ Fin)
54		inss1 4228	. . . . . . . 8 ⊢ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴
55		ssfi 9170	. . . . . . . 8 ⊢ ((∪ 𝐴 ∈ Fin ∧ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
56	53, 54, 55	sylancl 587	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
57		hashcl 14313	. . . . . . 7 ⊢ ((∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
58	56, 57	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
59	58	nn0cnd 12531	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℂ)
60	52, 59	mulcld 11231	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) ∈ ℂ)
61	39, 46, 7, 60	fsumsplit 15684	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
62		inidm 4218	. . . . . . 7 ⊢ (∪ 𝐴 ∩ ∪ 𝐴) = ∪ 𝐴
63	62	fveq2i 6892	. . . . . 6 ⊢ (♯‘(∪ 𝐴 ∩ ∪ 𝐴)) = (♯‘∪ 𝐴)
64	63	oveq2i 7417	. . . . 5 ⊢ ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = ((♯‘∪ 𝐴) − (♯‘∪ 𝐴))
65	4	subidd 11556	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘∪ 𝐴)) = 0)
66	64, 65	eqtrid 2785	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = 0)
67		incexclem 15779	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ ∪ 𝐴 ∈ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
68	1, 67	syldan 592	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
69	66, 68	eqtr3d 2775	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 0 = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
70	4, 37	negsubd 11574	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))))
71		0ex 5307	. . . . . . 7 ⊢ ∅ ∈ V
72		1cnd 11206	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 1 ∈ ℂ)
73	72, 4	mulcld 11231	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) ∈ ℂ)
74		fveq2 6889	. . . . . . . . . . . 12 ⊢ (𝑠 = ∅ → (♯‘𝑠) = (♯‘∅))
75		hash0 14324	. . . . . . . . . . . 12 ⊢ (♯‘∅) = 0
76	74, 75	eqtrdi 2789	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (♯‘𝑠) = 0)
77	76	oveq2d 7422	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = (-1↑0))
78		neg1cn 12323	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
79		exp0 14028	. . . . . . . . . . 11 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
80	78, 79	ax-mp 5	. . . . . . . . . 10 ⊢ (-1↑0) = 1
81	77, 80	eqtrdi 2789	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = 1)
82		rint0 4994	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (∪ 𝐴 ∩ ∩ 𝑠) = ∪ 𝐴)
83	82	fveq2d 6893	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∪ 𝐴))
84	81, 83	oveq12d 7424	. . . . . . . 8 ⊢ (𝑠 = ∅ → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
85	84	sumsn 15689	. . . . . . 7 ⊢ ((∅ ∈ V ∧ (1 · (♯‘∪ 𝐴)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
86	71, 73, 85	sylancr 588	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
87	4	mullidd 11229	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) = (♯‘∪ 𝐴))
88	86, 87	eqtr2d 2774	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
89	9, 36	fsumneg 15730	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
90		expm1t 14053	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ (♯‘𝑠) ∈ ℕ) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
91	11, 21, 90	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
92	24, 11	mulcomd 11232	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · -1) = (-1 · (-1↑((♯‘𝑠) − 1))))
93	24	mulm1d 11663	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1 · (-1↑((♯‘𝑠) − 1))) = -(-1↑((♯‘𝑠) − 1)))
94	91, 92, 93	3eqtrd 2777	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = -(-1↑((♯‘𝑠) − 1)))
95	25	unissd 4918	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ⊆ ∪ 𝐴)
96	31, 95	sstrd 3992	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝐴)
97		sseqin2 4215	. . . . . . . . . . 11 ⊢ (∩ 𝑠 ⊆ ∪ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
98	96, 97	sylib 217	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
99	98	fveq2d 6893	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∩ 𝑠))
100	94, 99	oveq12d 7424	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
101	24, 35	mulneg1d 11664	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
102	100, 101	eqtr2d 2774	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
103	102	sumeq2dv 15646	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
104	89, 103	eqtr3d 2775	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
105	88, 104	oveq12d 7424	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
106	70, 105	eqtr3d 2775	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
107	61, 69, 106	3eqtr4rd 2784	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = 0)
108	4, 37, 107	subeq0d 11576	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 Vcvv 3475 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 𝒫 cpw 4602 {csn 4628 ∪ cuni 4908 ∩ cint 4950 ‘cfv 6541 (class class class)co 7406 Fincfn 8936 ℂcc 11105 0cc0 11107 1c1 11108 + caddc 11110 · cmul 11112 − cmin 11441 -cneg 11442 ℕcn 12209 ℕ₀cn0 12469 ↑cexp 14024 ♯chash 14287 Σcsu 15629

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-om 7853 df-1st 7972 df-2nd 7973 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-oadd 8467 df-er 8700 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-sup 9434 df-oi 9502 df-dju 9893 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-n0 12470 df-z 12556 df-uz 12820 df-rp 12972 df-fz 13482 df-fzo 13625 df-seq 13964 df-exp 14025 df-hash 14288 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-clim 15429 df-sum 15630

This theorem is referenced by: incexc2 15781

W3C validator