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		incom	$$⊢\left(B\setminus A\right)\cap A=A\cap \left(B\setminus A\right)$$
10		disjdif	$$⊢A\cap \left(B\setminus A\right)=\varnothing$$
11	9 10	eqtri	$$⊢\left(B\setminus A\right)\cap A=\varnothing$$
12		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$$
13	8 11 12	mp2an	$$⊢\left(B\setminus A\right)\cap \left(A\cap B\right)=\varnothing$$
14	13	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$$
15		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|$$
16	2 6 14 15	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|$$
17		incom	$$⊢A\cap B=B\cap A$$
18	17	uneq2i	$$⊢\left(B\setminus A\right)\cup \left(A\cap B\right)=\left(B\setminus A\right)\cup \left(B\cap A\right)$$
19		uncom	$$⊢\left(B\setminus A\right)\cup \left(B\cap A\right)=\left(B\cap A\right)\cup \left(B\setminus A\right)$$
20		inundif	$$⊢\left(B\cap A\right)\cup \left(B\setminus A\right)=B$$
21	18 19 20	3eqtri	$$⊢\left(B\setminus A\right)\cup \left(A\cap B\right)=B$$
22	21	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$$
23	22	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|$$
24	16 23	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|$$
25		hashcl	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in {\mathbb{N}}_0$$
26	25	adantl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\right|\in {\mathbb{N}}_0$$
27	26	nn0cnd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\right|\in ℂ$$
28		hashcl	$$⊢A\cap B\in \mathrm{Fin}\to \left|A\cap B\right|\in {\mathbb{N}}_0$$
29	6 28	syl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cap B\right|\in {\mathbb{N}}_0$$
30	29	nn0cnd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cap B\right|\in ℂ$$
31		hashcl	$$⊢B\setminus A\in \mathrm{Fin}\to \left|B\setminus A\right|\in {\mathbb{N}}_0$$
32	2 31	syl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\setminus A\right|\in {\mathbb{N}}_0$$
33	32	nn0cnd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\setminus A\right|\in ℂ$$
34	27 30 33	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)$$
35	24 34	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|$$
36	35	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|$$
37		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
38	37	adantr	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\right|\in {\mathbb{N}}_0$$
39	38	nn0cnd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\right|\in ℂ$$
40	39 27 30	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|$$
41		undif2	$$⊢A\cup \left(B\setminus A\right)=A\cup B$$
42	41	fveq2i	$$⊢\left|A\cup \left(B\setminus A\right)\right|=\left|A\cup B\right|$$
43	10	a1i	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\cap \left(B\setminus A\right)=\varnothing$$
44		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|$$
45	3 2 43 44	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|$$
46	42 45	syl5eqr	$$⊢\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|$$
47	36 40 46	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|$$