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 15891

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 9301	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴 ∈ Fin)
2		hashcl 14392	. . . 4 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℕ₀)
3	2	nn0cnd 12567	. . 3 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℂ)
4	1, 3	syl 18	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) ∈ ℂ)
5		simpl 487	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
6		pwfi 9278	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
7	5, 6	sylib 221	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 ∈ Fin)
8		diffi 9159	. . . 4 ⊢ (𝒫 𝐴 ∈ Fin → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
9	7, 8	syl 18	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
10		1cnd 11202	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 1 ∈ ℂ)
11	10	negcld 11556	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -1 ∈ ℂ)
12		eldifsni 4760	. . . . . . . 8 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ≠ ∅)
13	12	adantl 486	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ≠ ∅)
14		eldifi 4091	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ∈ 𝒫 𝐴)
15		elpwi 4572	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴)
16	14, 15	syl 18	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ⊆ 𝐴)
17		ssfi 9157	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin)
18	5, 16, 17	syl2an 607	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ∈ Fin)
19		hashnncl 14402	. . . . . . . 8 ⊢ (𝑠 ∈ Fin → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
20	18, 19	syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
21	13, 20	mpbird 260	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘𝑠) ∈ ℕ)
22		nnm1nn0 12545	. . . . . 6 ⊢ ((♯‘𝑠) ∈ ℕ → ((♯‘𝑠) − 1) ∈ ℕ₀)
23	21, 22	syl 18	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) − 1) ∈ ℕ₀)
24	11, 23	expcld 14182	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑((♯‘𝑠) − 1)) ∈ ℂ)
25	16	adantl 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ 𝐴)
26		simplr 780	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝐴 ⊆ Fin)
27	25, 26	sstrd 3953	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ Fin)
28		unifi 9301	. . . . . . . 8 ⊢ ((𝑠 ∈ Fin ∧ 𝑠 ⊆ Fin) → ∪ 𝑠 ∈ Fin)
29	18, 27, 28	syl2anc 595	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ∈ Fin)
30		intssuni 4937	. . . . . . . 8 ⊢ (𝑠 ≠ ∅ → ∩ 𝑠 ⊆ ∪ 𝑠)
31	13, 30	syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝑠)
32	29, 31	ssfid 9229	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ∈ Fin)
33		hashcl 14392	. . . . . 6 ⊢ (∩ 𝑠 ∈ Fin → (♯‘∩ 𝑠) ∈ ℕ₀)
34	32, 33	syl 18	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℕ₀)
35	34	nn0cnd 12567	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℂ)
36	24, 35	mulcld 11229	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
37	9, 36	fsumcl 15784	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
38		disjdif 4436	. . . . 5 ⊢ ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅
39	38	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅)
40		0elpw 5327	. . . . . . . 8 ⊢ ∅ ∈ 𝒫 𝐴
41		snssi 4754	. . . . . . . 8 ⊢ (∅ ∈ 𝒫 𝐴 → {∅} ⊆ 𝒫 𝐴)
42	40, 41	ax-mp 5	. . . . . . 7 ⊢ {∅} ⊆ 𝒫 𝐴
43		undif 4446	. . . . . . 7 ⊢ ({∅} ⊆ 𝒫 𝐴 ↔ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴)
44	42, 43	mpbi 233	. . . . . 6 ⊢ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴
45	44	eqcomi 2778	. . . . 5 ⊢ 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅}))
46	45	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅})))
47		1cnd 11202	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 1 ∈ ℂ)
48	47	negcld 11556	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → -1 ∈ ℂ)
49	5, 15, 17	syl2an 607	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑠 ∈ Fin)
50		hashcl 14392	. . . . . . 7 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
51	49, 50	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘𝑠) ∈ ℕ₀)
52	48, 51	expcld 14182	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (-1↑(♯‘𝑠)) ∈ ℂ)
53	1	adantr 485	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ∪ 𝐴 ∈ Fin)
54		inss1 4195	. . . . . . . 8 ⊢ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴
55		ssfi 9157	. . . . . . . 8 ⊢ ((∪ 𝐴 ∈ Fin ∧ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
56	53, 54, 55	sylancl 597	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
57		hashcl 14392	. . . . . . 7 ⊢ ((∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
58	56, 57	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
59	58	nn0cnd 12567	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℂ)
60	52, 59	mulcld 11229	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) ∈ ℂ)
61	39, 46, 7, 60	fsumsplit 15792	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
62		inidm 4185	. . . . . . 7 ⊢ (∪ 𝐴 ∩ ∪ 𝐴) = ∪ 𝐴
63	62	fveq2i 6885	. . . . . 6 ⊢ (♯‘(∪ 𝐴 ∩ ∪ 𝐴)) = (♯‘∪ 𝐴)
64	63	oveq2i 7422	. . . . 5 ⊢ ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = ((♯‘∪ 𝐴) − (♯‘∪ 𝐴))
65	4	subidd 11557	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘∪ 𝐴)) = 0)
66	64, 65	eqtrid 2816	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = 0)
67		incexclem 15890	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ ∪ 𝐴 ∈ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
68	1, 67	syldan 602	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
69	66, 68	eqtr3d 2806	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 0 = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
70	4, 37	negsubd 11575	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))))
71		0ex 5272	. . . . . . 7 ⊢ ∅ ∈ V
72		1cnd 11202	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 1 ∈ ℂ)
73	72, 4	mulcld 11229	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) ∈ ℂ)
74		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑠 = ∅ → (♯‘𝑠) = (♯‘∅))
75		hash0 14403	. . . . . . . . . . . 12 ⊢ (♯‘∅) = 0
76	74, 75	eqtrdi 2820	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (♯‘𝑠) = 0)
77	76	oveq2d 7427	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = (-1↑0))
78		neg1cn 12203	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
79		exp0 14101	. . . . . . . . . . 11 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
80	78, 79	ax-mp 5	. . . . . . . . . 10 ⊢ (-1↑0) = 1
81	77, 80	eqtrdi 2820	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = 1)
82		rint0 4955	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (∪ 𝐴 ∩ ∩ 𝑠) = ∪ 𝐴)
83	82	fveq2d 6886	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∪ 𝐴))
84	81, 83	oveq12d 7429	. . . . . . . 8 ⊢ (𝑠 = ∅ → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
85	84	sumsn 15797	. . . . . . 7 ⊢ ((∅ ∈ V ∧ (1 · (♯‘∪ 𝐴)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
86	71, 73, 85	sylancr 598	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
87	4	mullidd 11227	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) = (♯‘∪ 𝐴))
88	86, 87	eqtr2d 2805	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
89	9, 36	fsumneg 15838	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
90		expm1t 14126	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ (♯‘𝑠) ∈ ℕ) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
91	11, 21, 90	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
92	24, 11	mulcomd 11230	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · -1) = (-1 · (-1↑((♯‘𝑠) − 1))))
93	24	mulm1d 11666	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1 · (-1↑((♯‘𝑠) − 1))) = -(-1↑((♯‘𝑠) − 1)))
94	91, 92, 93	3eqtrd 2808	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = -(-1↑((♯‘𝑠) − 1)))
95	25	unissd 4884	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ⊆ ∪ 𝐴)
96	31, 95	sstrd 3953	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝐴)
97		sseqin2 4182	. . . . . . . . . . 11 ⊢ (∩ 𝑠 ⊆ ∪ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
98	96, 97	sylib 221	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
99	98	fveq2d 6886	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∩ 𝑠))
100	94, 99	oveq12d 7429	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
101	24, 35	mulneg1d 11667	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
102	100, 101	eqtr2d 2805	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
103	102	sumeq2dv 15753	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
104	89, 103	eqtr3d 2806	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
105	88, 104	oveq12d 7429	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
106	70, 105	eqtr3d 2806	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
107	61, 69, 106	3eqtr4rd 2815	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = 0)
108	4, 37, 107	subeq0d 11577	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 Vcvv 3461 ∖ cdif 3908 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 ∅c0 4292 𝒫 cpw 4565 {csn 4592 ∪ cuni 4874 ∩ cint 4914 ‘cfv 6537 (class class class)co 7411 Fincfn 8943 ℂcc 11098 0cc0 11100 1c1 11101 + caddc 11103 · cmul 11105 − cmin 11441 -cneg 11442 ℕcn 12233 ℕ₀cn0 12504 ↑cexp 14097 ♯chash 14366 Σcsu 15737

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9610 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-oadd 8457 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-sup 9402 df-oi 9472 df-dju 9887 df-card 9925 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-n0 12505 df-z 12592 df-uz 12863 df-rp 13017 df-fz 13536 df-fzo 13683 df-seq 14038 df-exp 14098 df-hash 14367 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287 df-clim 15539 df-sum 15738

This theorem is referenced by: incexc2 15892

W3C validator