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 15959

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 9311	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴 ∈ Fin)
2		hashcl 14453	. . . 4 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℕ₀)
3	2	nn0cnd 12624	. . 3 ⊢ (∪ 𝐴 ∈ Fin → (♯‘∪ 𝐴) ∈ ℂ)
4	1, 3	syl 18	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) ∈ ℂ)
5		simpl 488	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
6		pwfi 9288	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
7	5, 6	sylib 221	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 ∈ Fin)
8		diffi 9169	. . . 4 ⊢ (𝒫 𝐴 ∈ Fin → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
9	7, 8	syl 18	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫 𝐴 ∖ {∅}) ∈ Fin)
10		1cnd 11259	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 1 ∈ ℂ)
11	10	negcld 11613	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -1 ∈ ℂ)
12		eldifsni 4753	. . . . . . . 8 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ≠ ∅)
13	12	adantl 487	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ≠ ∅)
14		eldifi 4078	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ∈ 𝒫 𝐴)
15		elpwi 4564	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴)
16	14, 15	syl 18	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ⊆ 𝐴)
17		ssfi 9167	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin)
18	5, 16, 17	syl2an 608	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ∈ Fin)
19		hashnncl 14463	. . . . . . . 8 ⊢ (𝑠 ∈ Fin → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
20	18, 19	syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅))
21	13, 20	mpbird 260	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘𝑠) ∈ ℕ)
22		nnm1nn0 12602	. . . . . 6 ⊢ ((♯‘𝑠) ∈ ℕ → ((♯‘𝑠) − 1) ∈ ℕ₀)
23	21, 22	syl 18	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((♯‘𝑠) − 1) ∈ ℕ₀)
24	11, 23	expcld 14243	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑((♯‘𝑠) − 1)) ∈ ℂ)
25	16	adantl 487	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ 𝐴)
26		simplr 781	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝐴 ⊆ Fin)
27	25, 26	sstrd 3941	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 𝑠 ⊆ Fin)
28		unifi 9311	. . . . . . . 8 ⊢ ((𝑠 ∈ Fin ∧ 𝑠 ⊆ Fin) → ∪ 𝑠 ∈ Fin)
29	18, 27, 28	syl2anc 596	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ∈ Fin)
30		intssuni 4930	. . . . . . . 8 ⊢ (𝑠 ≠ ∅ → ∩ 𝑠 ⊆ ∪ 𝑠)
31	13, 30	syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝑠)
32	29, 31	ssfid 9239	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ∈ Fin)
33		hashcl 14453	. . . . . 6 ⊢ (∩ 𝑠 ∈ Fin → (♯‘∩ 𝑠) ∈ ℕ₀)
34	32, 33	syl 18	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℕ₀)
35	34	nn0cnd 12624	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘∩ 𝑠) ∈ ℂ)
36	24, 35	mulcld 11286	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
37	9, 36	fsumcl 15852	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) ∈ ℂ)
38		disjdif 4426	. . . . 5 ⊢ ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅
39	38	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ({∅} ∩ (𝒫 𝐴 ∖ {∅})) = ∅)
40		0elpw 5317	. . . . . . . 8 ⊢ ∅ ∈ 𝒫 𝐴
41		snssi 4746	. . . . . . . 8 ⊢ (∅ ∈ 𝒫 𝐴 → {∅} ⊆ 𝒫 𝐴)
42	40, 41	ax-mp 5	. . . . . . 7 ⊢ {∅} ⊆ 𝒫 𝐴
43		undif 4438	. . . . . . 7 ⊢ ({∅} ⊆ 𝒫 𝐴 ↔ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴)
44	42, 43	mpbi 233	. . . . . 6 ⊢ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴
45	44	eqcomi 2769	. . . . 5 ⊢ 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅}))
46	45	a1i 11	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫 𝐴 = ({∅} ∪ (𝒫 𝐴 ∖ {∅})))
47		1cnd 11259	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 1 ∈ ℂ)
48	47	negcld 11613	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → -1 ∈ ℂ)
49	5, 15, 17	syl2an 608	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑠 ∈ Fin)
50		hashcl 14453	. . . . . . 7 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
51	49, 50	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘𝑠) ∈ ℕ₀)
52	48, 51	expcld 14243	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (-1↑(♯‘𝑠)) ∈ ℂ)
53	1	adantr 486	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ∪ 𝐴 ∈ Fin)
54		inss1 4182	. . . . . . . 8 ⊢ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴
55		ssfi 9167	. . . . . . . 8 ⊢ ((∪ 𝐴 ∈ Fin ∧ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
56	53, 54, 55	sylancl 598	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin)
57		hashcl 14453	. . . . . . 7 ⊢ ((∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
58	56, 57	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℕ₀)
59	58	nn0cnd 12624	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) ∈ ℂ)
60	52, 59	mulcld 11286	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) ∈ ℂ)
61	39, 46, 7, 60	fsumsplit 15860	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
62		inidm 4172	. . . . . . 7 ⊢ (∪ 𝐴 ∩ ∪ 𝐴) = ∪ 𝐴
63	62	fveq2i 6877	. . . . . 6 ⊢ (♯‘(∪ 𝐴 ∩ ∪ 𝐴)) = (♯‘∪ 𝐴)
64	63	oveq2i 7420	. . . . 5 ⊢ ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = ((♯‘∪ 𝐴) − (♯‘∪ 𝐴))
65	4	subidd 11614	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘∪ 𝐴)) = 0)
66	64, 65	eqtrid 2807	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = 0)
67		incexclem 15958	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ ∪ 𝐴 ∈ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
68	1, 67	syldan 603	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − (♯‘(∪ 𝐴 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
69	66, 68	eqtr3d 2797	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 0 = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
70	4, 37	negsubd 11632	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))))
71		0ex 5261	. . . . . . 7 ⊢ ∅ ∈ V
72		1cnd 11259	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 1 ∈ ℂ)
73	72, 4	mulcld 11286	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) ∈ ℂ)
74		fveq2 6874	. . . . . . . . . . . 12 ⊢ (𝑠 = ∅ → (♯‘𝑠) = (♯‘∅))
75		hash0 14464	. . . . . . . . . . . 12 ⊢ (♯‘∅) = 0
76	74, 75	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (♯‘𝑠) = 0)
77	76	oveq2d 7425	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = (-1↑0))
78		neg1cn 12260	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
79		exp0 14162	. . . . . . . . . . 11 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
80	78, 79	ax-mp 5	. . . . . . . . . 10 ⊢ (-1↑0) = 1
81	77, 80	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = 1)
82		rint0 4948	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (∪ 𝐴 ∩ ∩ 𝑠) = ∪ 𝐴)
83	82	fveq2d 6878	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∪ 𝐴))
84	81, 83	oveq12d 7427	. . . . . . . 8 ⊢ (𝑠 = ∅ → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
85	84	sumsn 15865	. . . . . . 7 ⊢ ((∅ ∈ V ∧ (1 · (♯‘∪ 𝐴)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
86	71, 73, 85	sylancr 599	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (♯‘∪ 𝐴)))
87	4	mullidd 11284	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 · (♯‘∪ 𝐴)) = (♯‘∪ 𝐴))
88	86, 87	eqtr2d 2796	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
89	9, 36	fsumneg 15906	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
90		expm1t 14187	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ (♯‘𝑠) ∈ ℕ) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
91	11, 21, 90	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = ((-1↑((♯‘𝑠) − 1)) · -1))
92	24, 11	mulcomd 11287	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑((♯‘𝑠) − 1)) · -1) = (-1 · (-1↑((♯‘𝑠) − 1))))
93	24	mulm1d 11723	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1 · (-1↑((♯‘𝑠) − 1))) = -(-1↑((♯‘𝑠) − 1)))
94	91, 92, 93	3eqtrd 2799	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1↑(♯‘𝑠)) = -(-1↑((♯‘𝑠) − 1)))
95	25	unissd 4877	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∪ 𝑠 ⊆ ∪ 𝐴)
96	31, 95	sstrd 3941	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ∩ 𝑠 ⊆ ∪ 𝐴)
97		sseqin2 4169	. . . . . . . . . . 11 ⊢ (∩ 𝑠 ⊆ ∪ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
98	96, 97	sylib 221	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (∪ 𝐴 ∩ ∩ 𝑠) = ∩ 𝑠)
99	98	fveq2d 6878	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (♯‘(∪ 𝐴 ∩ ∩ 𝑠)) = (♯‘∩ 𝑠))
100	94, 99	oveq12d 7427	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) = (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
101	24, 35	mulneg1d 11724	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-(-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)))
102	100, 101	eqtr2d 2796	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
103	102	sumeq2dv 15822	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})-((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
104	89, 103	eqtr3d 2797	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠)) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))))
105	88, 104	oveq12d 7427	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
106	70, 105	eqtr3d 2797	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(♯‘𝑠)) · (♯‘(∪ 𝐴 ∩ ∩ 𝑠)))))
107	61, 69, 106	3eqtr4rd 2806	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ((♯‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) = 0)
108	4, 37, 107	subeq0d 11635	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 2955 Vcvv 3450 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 𝒫 cpw 4557 {csn 4584 ∪ cuni 4867 ∩ cint 4907 ‘cfv 6528 (class class class)co 7409 Fincfn 8952 ℂcc 11155 0cc0 11157 1c1 11158 + caddc 11160 · cmul 11162 − cmin 11498 -cneg 11499 ℕcn 12290 ℕ₀cn0 12561 ↑cexp 14158 ♯chash 14427 Σcsu 15806

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 2213 ax-ext 2732 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7735 ax-inf2 9620 ax-cnex 11213 ax-resscn 11214 ax-1cn 11215 ax-icn 11216 ax-addcl 11217 ax-addrcl 11218 ax-mulcl 11219 ax-mulrcl 11220 ax-mulcom 11221 ax-addass 11222 ax-mulass 11223 ax-distr 11224 ax-i2m1 11225 ax-1ne0 11226 ax-1rid 11227 ax-rnegex 11228 ax-rrecex 11229 ax-cnre 11230 ax-pre-lttri 11231 ax-pre-lttrn 11232 ax-pre-ltadd 11233 ax-pre-mulgt0 11234 ax-pre-sup 11235

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 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-se 5602 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6294 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6530 df-fn 6531 df-f 6532 df-f1 6533 df-fo 6534 df-f1o 6535 df-fv 6536 df-isom 6537 df-riota 7366 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8455 df-oadd 8459 df-er 8696 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-oi 9482 df-dju 9939 df-card 9977 df-pnf 11302 df-mnf 11303 df-xr 11304 df-ltxr 11305 df-le 11306 df-sub 11500 df-neg 11501 df-div 11929 df-nn 12291 df-2 12360 df-3 12361 df-n0 12562 df-z 12649 df-uz 12921 df-rp 13076 df-fz 13595 df-fzo 13743 df-seq 14099 df-exp 14159 df-hash 14428 df-cj 15219 df-re 15220 df-im 15221 df-sqrt 15355 df-abs 15356 df-clim 15608 df-sum 15807

This theorem is used by: incexc2 15960

W3C validator