Theorem hashun3

Description: The size of the union of finite sets is the sum of their sizes minus the size of the intersection. (Contributed by Mario Carneiro, 6-Aug-2017)

	Ref	Expression
Assertion	hashun3	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cup B\right|=\left|A\right|+\left|B\right|-\left|A\cap B\right|$$

Proof

Step	Hyp	Ref	Expression
1		diffi	$$⊢B\in \mathrm{Fin}\to B\setminus A\in \mathrm{Fin}$$
2	1	adantl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to B\setminus A\in \mathrm{Fin}$$
3		simpl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\in \mathrm{Fin}$$
4		inss1	$$⊢A\cap B\subseteq A$$
5		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge A\cap B\subseteq A\right)\to A\cap B\in \mathrm{Fin}$$
6	3 4 5	sylancl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\cap B\in \mathrm{Fin}$$
7		sslin	$$⊢A\cap B\subseteq A\to \left(B\setminus A\right)\cap \left(A\cap B\right)\subseteq \left(B\setminus A\right)\cap A$$
8	4 7	ax-mp	$$⊢\left(B\setminus A\right)\cap \left(A\cap B\right)\subseteq \left(B\setminus A\right)\cap A$$
9		disjdifr	$$⊢\left(B\setminus A\right)\cap A=\varnothing$$
10		sseq0	$$⊢\left(\left(B\setminus A\right)\cap \left(A\cap B\right)\subseteq \left(B\setminus A\right)\cap A\wedge \left(B\setminus A\right)\cap A=\varnothing \right)\to \left(B\setminus A\right)\cap \left(A\cap B\right)=\varnothing$$
11	8 9 10	mp2an	$$⊢\left(B\setminus A\right)\cap \left(A\cap B\right)=\varnothing$$
12	11	a1i	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(B\setminus A\right)\cap \left(A\cap B\right)=\varnothing$$
13		hashun	$$⊢\left(B\setminus A\in \mathrm{Fin}\wedge A\cap B\in \mathrm{Fin}\wedge \left(B\setminus A\right)\cap \left(A\cap B\right)=\varnothing \right)\to \left|\left(B\setminus A\right)\cup \left(A\cap B\right)\right|=\left|B\setminus A\right|+\left|A\cap B\right|$$
14	2 6 12 13	syl3anc	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|\left(B\setminus A\right)\cup \left(A\cap B\right)\right|=\left|B\setminus A\right|+\left|A\cap B\right|$$
15		incom	$$⊢A\cap B=B\cap A$$
16	15	uneq2i	$$⊢\left(B\setminus A\right)\cup \left(A\cap B\right)=\left(B\setminus A\right)\cup \left(B\cap A\right)$$
17		uncom	$$⊢\left(B\setminus A\right)\cup \left(B\cap A\right)=\left(B\cap A\right)\cup \left(B\setminus A\right)$$
18		inundif	$$⊢\left(B\cap A\right)\cup \left(B\setminus A\right)=B$$
19	16 17 18	3eqtri	$$⊢\left(B\setminus A\right)\cup \left(A\cap B\right)=B$$
20	19	a1i	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(B\setminus A\right)\cup \left(A\cap B\right)=B$$
21	20	fveq2d	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|\left(B\setminus A\right)\cup \left(A\cap B\right)\right|=\left|B\right|$$
22	14 21	eqtr3d	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\setminus A\right|+\left|A\cap B\right|=\left|B\right|$$
23		hashcl	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in {\mathbb{N}}_0$$
24	23	adantl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\right|\in {\mathbb{N}}_0$$
25	24	nn0cnd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\right|\in ℂ$$
26		hashcl	$$⊢A\cap B\in \mathrm{Fin}\to \left|A\cap B\right|\in {\mathbb{N}}_0$$
27	6 26	syl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cap B\right|\in {\mathbb{N}}_0$$
28	27	nn0cnd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cap B\right|\in ℂ$$
29		hashcl	$$⊢B\setminus A\in \mathrm{Fin}\to \left|B\setminus A\right|\in {\mathbb{N}}_0$$
30	2 29	syl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\setminus A\right|\in {\mathbb{N}}_0$$
31	30	nn0cnd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\setminus A\right|\in ℂ$$
32	25 28 31	subadd2d	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|B\right|-\left|A\cap B\right|=\left|B\setminus A\right|\leftrightarrow \left|B\setminus A\right|+\left|A\cap B\right|=\left|B\right|\right)$$
33	22 32	mpbird	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\right|-\left|A\cap B\right|=\left|B\setminus A\right|$$
34	33	oveq2d	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\right|+\left|B\right|-\left|A\cap B\right|=\left|A\right|+\left|B\setminus A\right|$$
35		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
36	35	adantr	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\right|\in {\mathbb{N}}_0$$
37	36	nn0cnd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\right|\in ℂ$$
38	37 25 28	addsubassd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\right|+\left|B\right|-\left|A\cap B\right|=\left|A\right|+\left|B\right|-\left|A\cap B\right|$$
39		undif2	$$⊢A\cup \left(B\setminus A\right)=A\cup B$$
40	39	fveq2i	$$⊢\left|A\cup \left(B\setminus A\right)\right|=\left|A\cup B\right|$$
41		disjdif	$$⊢A\cap \left(B\setminus A\right)=\varnothing$$
42	41	a1i	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\cap \left(B\setminus A\right)=\varnothing$$
43		hashun	$$⊢\left(A\in \mathrm{Fin}\wedge B\setminus A\in \mathrm{Fin}\wedge A\cap \left(B\setminus A\right)=\varnothing \right)\to \left|A\cup \left(B\setminus A\right)\right|=\left|A\right|+\left|B\setminus A\right|$$
44	3 2 42 43	syl3anc	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cup \left(B\setminus A\right)\right|=\left|A\right|+\left|B\setminus A\right|$$
45	40 44	eqtr3id	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cup B\right|=\left|A\right|+\left|B\setminus A\right|$$
46	34 38 45	3eqtr4rd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cup B\right|=\left|A\right|+\left|B\right|-\left|A\cap B\right|$$