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 15928

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 9314	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴 ∈ Fin)
2		hashcl 14422	. . . 4 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℕ₀)
3	2	nn0cnd 12594	. . 3 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℂ)
4	1, 3	syl 18	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) ∈ ℂ)
5		simpl 488	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
6		pwfi 9291	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
7	5, 6	sylib 221	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 ∈ Fin)
8		diffi 9172	. . . 4 ⊢ (𝒫 𝐴 ∈ Fin → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
9	7, 8	syl 18	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
10		1cnd 11229	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 1 ∈ ℂ)
11	10	negcld 11583	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -1 ∈ ℂ)
12		eldifsni 4756	. . . . . . . 8 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ≠ ∅)
13	12	adantl 487	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ≠ ∅)
14		eldifi 4081	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ∈ 𝒫 𝐴)
15		elpwi 4567	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴)
16	14, 15	syl 18	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ⊆ 𝐴)
17		ssfi 9170	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin)
18	5, 16, 17	syl2an 608	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ∈ Fin)
19		hashnncl 14432	. . . . . . . 8 ⊢ (𝑠 ∈ Fin → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
20	18, 19	syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
21	13, 20	mpbird 260	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘𝑠) ∈ ℕ)
22		nnm1nn0 12572	. . . . . 6 ⊢ ((♯‘𝑠) ∈ ℕ → ((♯‘𝑠) − 1) ∈ ℕ₀)
23	21, 22	syl 18	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) − 1) ∈ ℕ₀)
24	11, 23	expcld 14212	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑((♯‘𝑠) − 1)) ∈ ℂ)
25	16	adantl 487	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ 𝐴)
26		simplr 781	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝐴 ⊆ Fin)
27	25, 26	sstrd 3944	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ Fin)
28		unifi 9314	. . . . . . . 8 ⊢ ((𝑠 ∈ Fin ∧ 𝑠 ⊆ Fin) → ∪ 𝑠 ∈ Fin)
29	18, 27, 28	syl2anc 596	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ∈ Fin)
30		intssuni 4933	. . . . . . . 8 ⊢ (𝑠 ≠ ∅ → ∩ 𝑠 ⊆ ∪ 𝑠)
31	13, 30	syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝑠)
32	29, 31	ssfid 9242	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ∈ Fin)
33		hashcl 14422	. . . . . 6 ⊢ (∩ 𝑠 ∈ Fin → (♯‘∩ 𝑠) ∈ ℕ₀)
34	32, 33	syl 18	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℕ₀)
35	34	nn0cnd 12594	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℂ)
36	24, 35	mulcld 11256	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
37	9, 36	fsumcl 15821	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
38		disjdif 4429	. . . . 5 ⊢ ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅
39	38	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅)
40		0elpw 5324	. . . . . . . 8 ⊢ ∅ ∈ 𝒫 𝐴
41		snssi 4749	. . . . . . . 8 ⊢ (∅ ∈ 𝒫 𝐴 → {∅} ⊆ 𝒫 𝐴)
42	40, 41	ax-mp 5	. . . . . . 7 ⊢ {∅} ⊆ 𝒫 𝐴
43		undif 4441	. . . . . . 7 ⊢ ({∅} ⊆ 𝒫 𝐴 ↔ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴)
44	42, 43	mpbi 233	. . . . . 6 ⊢ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴
45	44	eqcomi 2771	. . . . 5 ⊢ 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅}))
46	45	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅})))
47		1cnd 11229	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 1 ∈ ℂ)
48	47	negcld 11583	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → -1 ∈ ℂ)
49	5, 15, 17	syl2an 608	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑠 ∈ Fin)
50		hashcl 14422	. . . . . . 7 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
51	49, 50	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘𝑠) ∈ ℕ₀)
52	48, 51	expcld 14212	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (-1↑(♯‘𝑠)) ∈ ℂ)
53	1	adantr 486	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ∪ 𝐴 ∈ Fin)
54		inss1 4185	. . . . . . . 8 ⊢ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴
55		ssfi 9170	. . . . . . . 8 ⊢ ((∪ 𝐴 ∈ Fin ∧ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
56	53, 54, 55	sylancl 598	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
57		hashcl 14422	. . . . . . 7 ⊢ ((∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
58	56, 57	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
59	58	nn0cnd 12594	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℂ)
60	52, 59	mulcld 11256	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) ∈ ℂ)
61	39, 46, 7, 60	fsumsplit 15829	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
62		inidm 4175	. . . . . . 7 ⊢ (∪ 𝐴 ∩ ∪ 𝐴) = ∪ 𝐴
63	62	fveq2i 6885	. . . . . 6 ⊢ (♯‘(∪ 𝐴 ∩ ∪ 𝐴)) = (♯‘∪ 𝐴)
64	63	oveq2i 7427	. . . . 5 ⊢ ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = ((♯‘∪ 𝐴) − (♯‘∪ 𝐴))
65	4	subidd 11584	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘∪ 𝐴)) = 0)
66	64, 65	eqtrid 2809	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = 0)
67		incexclem 15927	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ ∪ 𝐴 ∈ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
68	1, 67	syldan 603	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
69	66, 68	eqtr3d 2799	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 0 = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
70	4, 37	negsubd 11602	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))))
71		0ex 5268	. . . . . . 7 ⊢ ∅ ∈ V
72		1cnd 11229	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 1 ∈ ℂ)
73	72, 4	mulcld 11256	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) ∈ ℂ)
74		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑠 = ∅ → (♯‘𝑠) = (♯‘∅))
75		hash0 14433	. . . . . . . . . . . 12 ⊢ (♯‘∅) = 0
76	74, 75	eqtrdi 2813	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (♯‘𝑠) = 0)
77	76	oveq2d 7432	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = (-1↑0))
78		neg1cn 12230	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
79		exp0 14131	. . . . . . . . . . 11 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
80	78, 79	ax-mp 5	. . . . . . . . . 10 ⊢ (-1↑0) = 1
81	77, 80	eqtrdi 2813	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = 1)
82		rint0 4951	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (∪ 𝐴 ∩ ∩ 𝑠) = ∪ 𝐴)
83	82	fveq2d 6886	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∪ 𝐴))
84	81, 83	oveq12d 7434	. . . . . . . 8 ⊢ (𝑠 = ∅ → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
85	84	sumsn 15834	. . . . . . 7 ⊢ ((∅ ∈ V ∧ (1 · (♯‘∪ 𝐴)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
86	71, 73, 85	sylancr 599	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
87	4	mullidd 11254	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) = (♯‘∪ 𝐴))
88	86, 87	eqtr2d 2798	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
89	9, 36	fsumneg 15875	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
90		expm1t 14156	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ (♯‘𝑠) ∈ ℕ) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
91	11, 21, 90	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
92	24, 11	mulcomd 11257	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · -1) = (-1 · (-1↑((♯‘𝑠) − 1))))
93	24	mulm1d 11693	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1 · (-1↑((♯‘𝑠) − 1))) = -(-1↑((♯‘𝑠) − 1)))
94	91, 92, 93	3eqtrd 2801	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = -(-1↑((♯‘𝑠) − 1)))
95	25	unissd 4880	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ⊆ ∪ 𝐴)
96	31, 95	sstrd 3944	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝐴)
97		sseqin2 4172	. . . . . . . . . . 11 ⊢ (∩ 𝑠 ⊆ ∪ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
98	96, 97	sylib 221	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
99	98	fveq2d 6886	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∩ 𝑠))
100	94, 99	oveq12d 7434	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
101	24, 35	mulneg1d 11694	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
102	100, 101	eqtr2d 2798	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
103	102	sumeq2dv 15791	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
104	89, 103	eqtr3d 2799	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
105	88, 104	oveq12d 7434	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
106	70, 105	eqtr3d 2799	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
107	61, 69, 106	3eqtr4rd 2808	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = 0)
108	4, 37, 107	subeq0d 11604	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 𝒫 cpw 4560 {csn 4587 ∪ cuni 4870 ∩ cint 4910 ‘cfv 6537 (class class class)co 7416 Fincfn 8955 ℂcc 11125 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 − cmin 11468 -cneg 11469 ℕcn 12260 ℕ₀cn0 12531 ↑cexp 14127 ♯chash 14396 Σcsu 15775

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 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 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-oadd 8462 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-sup 9415 df-oi 9485 df-dju 9909 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-n0 12532 df-z 12619 df-uz 12891 df-rp 13045 df-fz 13564 df-fzo 13712 df-seq 14068 df-exp 14128 df-hash 14397 df-cj 15188 df-re 15189 df-im 15190 df-sqrt 15324 df-abs 15325 df-clim 15577 df-sum 15776

This theorem is used by: incexc2 15929

W3C validator