incexc

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)

		Ref	Expression
	Assertion	incexc	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| = \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|$

Proof

Step	Hyp	Ref	Expression
1		unifi	$⊢ (A \in Fin \land A \subseteq Fin) \to ⋃ A \in Fin$
2		hashcl	$⊢ ⋃ A \in Fin \to \|⋃ A\| \in ℕ_{0}$
3	2	nn0cnd	$⊢ ⋃ A \in Fin \to \|⋃ A\| \in ℂ$
4	1 3	syl	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| \in ℂ$
5		simpl	$⊢ (A \in Fin \land A \subseteq Fin) \to A \in Fin$
6		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
7	5 6	sylib	$⊢ (A \in Fin \land A \subseteq Fin) \to 𝒫 A \in Fin$
8		diffi	$⊢ 𝒫 A \in Fin \to 𝒫 A ∖ \{\emptyset\} \in Fin$
9	7 8	syl	$⊢ (A \in Fin \land A \subseteq Fin) \to 𝒫 A ∖ \{\emptyset\} \in Fin$
10		1cnd	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to 1 \in ℂ$
11	10	negcld	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to - 1 \in ℂ$
12		eldifsni	$⊢ s \in (𝒫 A ∖ \{\emptyset\}) \to s \neq \emptyset$
13	12	adantl	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to s \neq \emptyset$
14		eldifi	$⊢ s \in (𝒫 A ∖ \{\emptyset\}) \to s \in 𝒫 A$
15		elpwi	$⊢ s \in 𝒫 A \to s \subseteq A$
16	14 15	syl	$⊢ s \in (𝒫 A ∖ \{\emptyset\}) \to s \subseteq A$
17		ssfi	$⊢ (A \in Fin \land s \subseteq A) \to s \in Fin$
18	5 16 17	syl2an	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to s \in Fin$
19		hashnncl	$⊢ s \in Fin \to (\|s\| \in ℕ \leftrightarrow s \neq \emptyset)$
20	18 19	syl	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to (\|s\| \in ℕ \leftrightarrow s \neq \emptyset)$
21	13 20	mpbird	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to \|s\| \in ℕ$
22		nnm1nn0	$⊢ \|s\| \in ℕ \to \|s\| - 1 \in ℕ_{0}$
23	21 22	syl	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to \|s\| - 1 \in ℕ_{0}$
24	11 23	expcld	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to {(- 1)}^{\|s\| - 1} \in ℂ$
25	16	adantl	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to s \subseteq A$
26		simplr	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to A \subseteq Fin$
27	25 26	sstrd	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to s \subseteq Fin$
28		unifi	$⊢ (s \in Fin \land s \subseteq Fin) \to ⋃ s \in Fin$
29	18 27 28	syl2anc	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to ⋃ s \in Fin$
30		intssuni	$⊢ s \neq \emptyset \to ⋂ s \subseteq ⋃ s$
31	13 30	syl	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to ⋂ s \subseteq ⋃ s$
32	29 31	ssfid	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to ⋂ s \in Fin$
33		hashcl	$⊢ ⋂ s \in Fin \to \|⋂ s\| \in ℕ_{0}$
34	32 33	syl	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to \|⋂ s\| \in ℕ_{0}$
35	34	nn0cnd	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to \|⋂ s\| \in ℂ$
36	24 35	mulcld	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to {(- 1)}^{\|s\| - 1} \|⋂ s\| \in ℂ$
37	9 36	fsumcl	$⊢ (A \in Fin \land A \subseteq Fin) \to \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\| \in ℂ$
38		disjdif	$⊢ \{\emptyset\} \cap (𝒫 A ∖ \{\emptyset\}) = \emptyset$
39	38	a1i	$⊢ (A \in Fin \land A \subseteq Fin) \to \{\emptyset\} \cap (𝒫 A ∖ \{\emptyset\}) = \emptyset$
40		0elpw	$⊢ \emptyset \in 𝒫 A$
41		snssi	$⊢ \emptyset \in 𝒫 A \to \{\emptyset\} \subseteq 𝒫 A$
42	40 41	ax-mp	$⊢ \{\emptyset\} \subseteq 𝒫 A$
43		undif	$⊢ \{\emptyset\} \subseteq 𝒫 A \leftrightarrow \{\emptyset\} \cup (𝒫 A ∖ \{\emptyset\}) = 𝒫 A$
44	42 43	mpbi	$⊢ \{\emptyset\} \cup (𝒫 A ∖ \{\emptyset\}) = 𝒫 A$
45	44	eqcomi	$⊢ 𝒫 A = \{\emptyset\} \cup (𝒫 A ∖ \{\emptyset\})$
46	45	a1i	$⊢ (A \in Fin \land A \subseteq Fin) \to 𝒫 A = \{\emptyset\} \cup (𝒫 A ∖ \{\emptyset\})$
47		1cnd	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to 1 \in ℂ$
48	47	negcld	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to - 1 \in ℂ$
49	5 15 17	syl2an	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to s \in Fin$
50		hashcl	$⊢ s \in Fin \to \|s\| \in ℕ_{0}$
51	49 50	syl	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to \|s\| \in ℕ_{0}$
52	48 51	expcld	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to {(- 1)}^{\|s\|} \in ℂ$
53	1	adantr	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to ⋃ A \in Fin$
54		inss1	$⊢ ⋃ A \cap ⋂ s \subseteq ⋃ A$
55		ssfi	$⊢ (⋃ A \in Fin \land ⋃ A \cap ⋂ s \subseteq ⋃ A) \to ⋃ A \cap ⋂ s \in Fin$
56	53 54 55	sylancl	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to ⋃ A \cap ⋂ s \in Fin$
57		hashcl	$⊢ ⋃ A \cap ⋂ s \in Fin \to \|⋃ A \cap ⋂ s\| \in ℕ_{0}$
58	56 57	syl	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to \|⋃ A \cap ⋂ s\| \in ℕ_{0}$
59	58	nn0cnd	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to \|⋃ A \cap ⋂ s\| \in ℂ$
60	52 59	mulcld	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in 𝒫 A) \to {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\| \in ℂ$
61	39 46 7 60	fsumsplit	$⊢ (A \in Fin \land A \subseteq Fin) \to \sum_{s \in 𝒫 A} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\| = \sum_{s \in \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\| + \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
62		inidm	$⊢ ⋃ A \cap ⋃ A = ⋃ A$
63	62	fveq2i	$⊢ \|⋃ A \cap ⋃ A\| = \|⋃ A\|$
64	63	oveq2i	$⊢ \|⋃ A\| - \|⋃ A \cap ⋃ A\| = \|⋃ A\| - \|⋃ A\|$
65	4	subidd	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| - \|⋃ A\| = 0$
66	64 65	eqtrid	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| - \|⋃ A \cap ⋃ A\| = 0$
67		incexclem	$⊢ (A \in Fin \land ⋃ A \in Fin) \to \|⋃ A\| - \|⋃ A \cap ⋃ A\| = \sum_{s \in 𝒫 A} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
68	1 67	syldan	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| - \|⋃ A \cap ⋃ A\| = \sum_{s \in 𝒫 A} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
69	66 68	eqtr3d	$⊢ (A \in Fin \land A \subseteq Fin) \to 0 = \sum_{s \in 𝒫 A} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
70	4 37	negsubd	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| + (- \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|) = \|⋃ A\| - \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|$
71		0ex	$⊢ \emptyset \in V$
72		1cnd	$⊢ (A \in Fin \land A \subseteq Fin) \to 1 \in ℂ$
73	72 4	mulcld	$⊢ (A \in Fin \land A \subseteq Fin) \to 1 \|⋃ A\| \in ℂ$
74		fveq2	$⊢ s = \emptyset \to \|s\| = \|\emptyset\|$
75		hash0	$⊢ \|\emptyset\| = 0$
76	74 75	eqtrdi	$⊢ s = \emptyset \to \|s\| = 0$
77	76	oveq2d	$⊢ s = \emptyset \to {(- 1)}^{\|s\|} = {(- 1)}^{0}$
78		neg1cn	$⊢ - 1 \in ℂ$
79		exp0	$⊢ - 1 \in ℂ \to {(- 1)}^{0} = 1$
80	78 79	ax-mp	$⊢ {(- 1)}^{0} = 1$
81	77 80	eqtrdi	$⊢ s = \emptyset \to {(- 1)}^{\|s\|} = 1$
82		rint0	$⊢ s = \emptyset \to ⋃ A \cap ⋂ s = ⋃ A$
83	82	fveq2d	$⊢ s = \emptyset \to \|⋃ A \cap ⋂ s\| = \|⋃ A\|$
84	81 83	oveq12d	$⊢ s = \emptyset \to {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\| = 1 \|⋃ A\|$
85	84	sumsn	$⊢ (\emptyset \in V \land 1 \|⋃ A\| \in ℂ) \to \sum_{s \in \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\| = 1 \|⋃ A\|$
86	71 73 85	sylancr	$⊢ (A \in Fin \land A \subseteq Fin) \to \sum_{s \in \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\| = 1 \|⋃ A\|$
87	4	mulid2d	$⊢ (A \in Fin \land A \subseteq Fin) \to 1 \|⋃ A\| = \|⋃ A\|$
88	86 87	eqtr2d	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| = \sum_{s \in \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
89	9 36	fsumneg	$⊢ (A \in Fin \land A \subseteq Fin) \to \sum_{s \in 𝒫 A ∖ \{\emptyset\}} (- {(- 1)}^{\|s\| - 1} \|⋂ s\|) = - \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|$
90		expm1t	$⊢ (- 1 \in ℂ \land \|s\| \in ℕ) \to {(- 1)}^{\|s\|} = {(- 1)}^{\|s\| - 1} -1$
91	11 21 90	syl2anc	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to {(- 1)}^{\|s\|} = {(- 1)}^{\|s\| - 1} -1$
92	24 11	mulcomd	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to {(- 1)}^{\|s\| - 1} -1 = -1 {(- 1)}^{\|s\| - 1}$
93	24	mulm1d	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to -1 {(- 1)}^{\|s\| - 1} = - {(- 1)}^{\|s\| - 1}$
94	91 92 93	3eqtrd	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to {(- 1)}^{\|s\|} = - {(- 1)}^{\|s\| - 1}$
95	25	unissd	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to ⋃ s \subseteq ⋃ A$
96	31 95	sstrd	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to ⋂ s \subseteq ⋃ A$
97		sseqin2	$⊢ ⋂ s \subseteq ⋃ A \leftrightarrow ⋃ A \cap ⋂ s = ⋂ s$
98	96 97	sylib	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to ⋃ A \cap ⋂ s = ⋂ s$
99	98	fveq2d	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to \|⋃ A \cap ⋂ s\| = \|⋂ s\|$
100	94 99	oveq12d	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\| = (- {(- 1)}^{\|s\| - 1}) \|⋂ s\|$
101	24 35	mulneg1d	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to (- {(- 1)}^{\|s\| - 1}) \|⋂ s\| = - {(- 1)}^{\|s\| - 1} \|⋂ s\|$
102	100 101	eqtr2d	$⊢ ((A \in Fin \land A \subseteq Fin) \land s \in (𝒫 A ∖ \{\emptyset\})) \to - {(- 1)}^{\|s\| - 1} \|⋂ s\| = {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
103	102	sumeq2dv	$⊢ (A \in Fin \land A \subseteq Fin) \to \sum_{s \in 𝒫 A ∖ \{\emptyset\}} (- {(- 1)}^{\|s\| - 1} \|⋂ s\|) = \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
104	89 103	eqtr3d	$⊢ (A \in Fin \land A \subseteq Fin) \to - \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\| = \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
105	88 104	oveq12d	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| + (- \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|) = \sum_{s \in \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\| + \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
106	70 105	eqtr3d	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| - \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\| = \sum_{s \in \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\| + \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\|} \|⋃ A \cap ⋂ s\|$
107	61 69 106	3eqtr4rd	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| - \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\| = 0$
108	4 37 107	subeq0d	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| = \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|$

Metamath Proof Explorer

Theorem incexc

Proof