incexc2

Description: The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017)

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

Proof

Step	Hyp	Ref	Expression
1		incexc	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| = \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|$
2		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
3	2	ad2antrr	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to \|A\| \in ℕ_{0}$
4	3	nn0zd	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to \|A\| \in ℤ$
5		simpl	$⊢ (A \in Fin \land A \subseteq Fin) \to A \in Fin$
6		elpwi	$⊢ k \in 𝒫 A \to k \subseteq A$
7		ssdomg	$⊢ A \in Fin \to (k \subseteq A \to k ≼ A)$
8	7	imp	$⊢ (A \in Fin \land k \subseteq A) \to k ≼ A$
9	5 6 8	syl2an	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to k ≼ A$
10		hashdomi	$⊢ k ≼ A \to \|k\| \leq \|A\|$
11	9 10	syl	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to \|k\| \leq \|A\|$
12		fznn	$⊢ \|A\| \in ℤ \to (\|k\| \in (1 \dots \|A\|) \leftrightarrow (\|k\| \in ℕ \land \|k\| \leq \|A\|))$
13	12	rbaibd	$⊢ (\|A\| \in ℤ \land \|k\| \leq \|A\|) \to (\|k\| \in (1 \dots \|A\|) \leftrightarrow \|k\| \in ℕ)$
14	4 11 13	syl2anc	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to (\|k\| \in (1 \dots \|A\|) \leftrightarrow \|k\| \in ℕ)$
15		ssfi	$⊢ (A \in Fin \land k \subseteq A) \to k \in Fin$
16	5 6 15	syl2an	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to k \in Fin$
17		hashnncl	$⊢ k \in Fin \to (\|k\| \in ℕ \leftrightarrow k \neq \emptyset)$
18	16 17	syl	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to (\|k\| \in ℕ \leftrightarrow k \neq \emptyset)$
19	14 18	bitr2d	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to (k \neq \emptyset \leftrightarrow \|k\| \in (1 \dots \|A\|))$
20		df-ne	$⊢ k \neq \emptyset \leftrightarrow \neg k = \emptyset$
21		risset	$⊢ \|k\| \in (1 \dots \|A\|) \leftrightarrow \exists n \in (1 \dots \|A\|) n = \|k\|$
22	19 20 21	3bitr3g	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to (\neg k = \emptyset \leftrightarrow \exists n \in (1 \dots \|A\|) n = \|k\|)$
23		velsn	$⊢ k \in \{\emptyset\} \leftrightarrow k = \emptyset$
24	23	notbii	$⊢ \neg k \in \{\emptyset\} \leftrightarrow \neg k = \emptyset$
25		eqcom	$⊢ \|k\| = n \leftrightarrow n = \|k\|$
26	25	rexbii	$⊢ \exists n \in (1 \dots \|A\|) \|k\| = n \leftrightarrow \exists n \in (1 \dots \|A\|) n = \|k\|$
27	22 24 26	3bitr4g	$⊢ ((A \in Fin \land A \subseteq Fin) \land k \in 𝒫 A) \to (\neg k \in \{\emptyset\} \leftrightarrow \exists n \in (1 \dots \|A\|) \|k\| = n)$
28	27	rabbidva	$⊢ (A \in Fin \land A \subseteq Fin) \to \{k \in 𝒫 A \| \neg k \in \{\emptyset\}\} = \{k \in 𝒫 A \| \exists n \in (1 \dots \|A\|) \|k\| = n\}$
29		dfdif2	$⊢ 𝒫 A ∖ \{\emptyset\} = \{k \in 𝒫 A \| \neg k \in \{\emptyset\}\}$
30		iunrab	$⊢ ⋃_{n = 1}^{\|A\|} \{k \in 𝒫 A \| \|k\| = n\} = \{k \in 𝒫 A \| \exists n \in (1 \dots \|A\|) \|k\| = n\}$
31	28 29 30	3eqtr4g	$⊢ (A \in Fin \land A \subseteq Fin) \to 𝒫 A ∖ \{\emptyset\} = ⋃_{n = 1}^{\|A\|} \{k \in 𝒫 A \| \|k\| = n\}$
32	31	sumeq1d	$⊢ (A \in Fin \land A \subseteq Fin) \to \sum_{s \in 𝒫 A ∖ \{\emptyset\}} {(- 1)}^{\|s\| - 1} \|⋂ s\| = \sum_{s \in ⋃_{n = 1}^{\|A\|} \{k \in 𝒫 A \| \|k\| = n\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|$
33	1 32	eqtrd	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| = \sum_{s \in ⋃_{n = 1}^{\|A\|} \{k \in 𝒫 A \| \|k\| = n\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|$
34		fzfid	$⊢ (A \in Fin \land A \subseteq Fin) \to (1 \dots \|A\|) \in Fin$
35		simpll	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to A \in Fin$
36		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
37	35 36	sylib	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to 𝒫 A \in Fin$
38		ssrab2	$⊢ \{k \in 𝒫 A \| \|k\| = n\} \subseteq 𝒫 A$
39		ssfi	$⊢ (𝒫 A \in Fin \land \{k \in 𝒫 A \| \|k\| = n\} \subseteq 𝒫 A) \to \{k \in 𝒫 A \| \|k\| = n\} \in Fin$
40	37 38 39	sylancl	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to \{k \in 𝒫 A \| \|k\| = n\} \in Fin$
41		fveqeq2	$⊢ k = s \to (\|k\| = n \leftrightarrow \|s\| = n)$
42	41	elrab	$⊢ s \in \{k \in 𝒫 A \| \|k\| = n\} \leftrightarrow (s \in 𝒫 A \land \|s\| = n)$
43	42	simprbi	$⊢ s \in \{k \in 𝒫 A \| \|k\| = n\} \to \|s\| = n$
44	43	adantl	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to \|s\| = n$
45	44	ralrimiva	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to \forall s \in \{k \in 𝒫 A \| \|k\| = n\} \|s\| = n$
46	45	ralrimiva	$⊢ (A \in Fin \land A \subseteq Fin) \to \forall n \in (1 \dots \|A\|) \forall s \in \{k \in 𝒫 A \| \|k\| = n\} \|s\| = n$
47		invdisj	$⊢ \forall n \in (1 \dots \|A\|) \forall s \in \{k \in 𝒫 A \| \|k\| = n\} \|s\| = n \to {Disj}_{n = 1}^{\|A\|} \{k \in 𝒫 A \| \|k\| = n\}$
48	46 47	syl	$⊢ (A \in Fin \land A \subseteq Fin) \to {Disj}_{n = 1}^{\|A\|} \{k \in 𝒫 A \| \|k\| = n\}$
49	44	oveq1d	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to \|s\| - 1 = n - 1$
50	49	oveq2d	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to {(- 1)}^{\|s\| - 1} = {(- 1)}^{n - 1}$
51	50	oveq1d	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to {(- 1)}^{\|s\| - 1} \|⋂ s\| = {(- 1)}^{n - 1} \|⋂ s\|$
52		1cnd	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to 1 \in ℂ$
53	52	negcld	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to - 1 \in ℂ$
54		elfznn	$⊢ n \in (1 \dots \|A\|) \to n \in ℕ$
55	54	adantl	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to n \in ℕ$
56		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
57	55 56	syl	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to n - 1 \in ℕ_{0}$
58	53 57	expcld	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to {(- 1)}^{n - 1} \in ℂ$
59	58	adantr	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to {(- 1)}^{n - 1} \in ℂ$
60		unifi	$⊢ (A \in Fin \land A \subseteq Fin) \to ⋃ A \in Fin$
61	60	ad2antrr	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to ⋃ A \in Fin$
62	55	adantr	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to n \in ℕ$
63	44 62	eqeltrd	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to \|s\| \in ℕ$
64	35	adantr	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to A \in Fin$
65		elrabi	$⊢ s \in \{k \in 𝒫 A \| \|k\| = n\} \to s \in 𝒫 A$
66	65	adantl	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to s \in 𝒫 A$
67		elpwi	$⊢ s \in 𝒫 A \to s \subseteq A$
68	66 67	syl	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to s \subseteq A$
69	64 68	ssfid	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to s \in Fin$
70		hashnncl	$⊢ s \in Fin \to (\|s\| \in ℕ \leftrightarrow s \neq \emptyset)$
71	69 70	syl	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to (\|s\| \in ℕ \leftrightarrow s \neq \emptyset)$
72	63 71	mpbid	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to s \neq \emptyset$
73		intssuni	$⊢ s \neq \emptyset \to ⋂ s \subseteq ⋃ s$
74	72 73	syl	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to ⋂ s \subseteq ⋃ s$
75	68	unissd	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to ⋃ s \subseteq ⋃ A$
76	74 75	sstrd	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to ⋂ s \subseteq ⋃ A$
77	61 76	ssfid	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to ⋂ s \in Fin$
78		hashcl	$⊢ ⋂ s \in Fin \to \|⋂ s\| \in ℕ_{0}$
79	77 78	syl	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to \|⋂ s\| \in ℕ_{0}$
80	79	nn0cnd	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to \|⋂ s\| \in ℂ$
81	59 80	mulcld	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to {(- 1)}^{n - 1} \|⋂ s\| \in ℂ$
82	51 81	eqeltrd	$⊢ (((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \land s \in \{k \in 𝒫 A \| \|k\| = n\}) \to {(- 1)}^{\|s\| - 1} \|⋂ s\| \in ℂ$
83	82	anasss	$⊢ ((A \in Fin \land A \subseteq Fin) \land (n \in (1 \dots \|A\|) \land s \in \{k \in 𝒫 A \| \|k\| = n\})) \to {(- 1)}^{\|s\| - 1} \|⋂ s\| \in ℂ$
84	34 40 48 83	fsumiun	$⊢ (A \in Fin \land A \subseteq Fin) \to \sum_{s \in ⋃_{n = 1}^{\|A\|} \{k \in 𝒫 A \| \|k\| = n\}} {(- 1)}^{\|s\| - 1} \|⋂ s\| = \sum_{n = 1}^{\|A\|} \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} {(- 1)}^{\|s\| - 1} \|⋂ s\|$
85	51	sumeq2dv	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} {(- 1)}^{\|s\| - 1} \|⋂ s\| = \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} {(- 1)}^{n - 1} \|⋂ s\|$
86	40 58 80	fsummulc2	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to {(- 1)}^{n - 1} \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} \|⋂ s\| = \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} {(- 1)}^{n - 1} \|⋂ s\|$
87	85 86	eqtr4d	$⊢ ((A \in Fin \land A \subseteq Fin) \land n \in (1 \dots \|A\|)) \to \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} {(- 1)}^{\|s\| - 1} \|⋂ s\| = {(- 1)}^{n - 1} \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} \|⋂ s\|$
88	87	sumeq2dv	$⊢ (A \in Fin \land A \subseteq Fin) \to \sum_{n = 1}^{\|A\|} \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} {(- 1)}^{\|s\| - 1} \|⋂ s\| = \sum_{n = 1}^{\|A\|} {(- 1)}^{n - 1} \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} \|⋂ s\|$
89	33 84 88	3eqtrd	$⊢ (A \in Fin \land A \subseteq Fin) \to \|⋃ A\| = \sum_{n = 1}^{\|A\|} {(- 1)}^{n - 1} \sum_{s \in \{k \in 𝒫 A \| \|k\| = n\}} \|⋂ s\|$

Metamath Proof Explorer

Theorem incexc2

Proof