Theorem hashun2

Description: The size of the union of finite sets is less than or equal to the sum of their sizes. (Contributed by Mario Carneiro, 23-Sep-2013) (Proof shortened by Mario Carneiro, 27-Jul-2014)

	Ref	Expression
Assertion	hashun2	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cup B\right|\le \left|A\right|+\left|B\right|$$

Proof

Step	Hyp	Ref	Expression
1		undif2	$$⊢A\cup \left(B\setminus A\right)=A\cup B$$
2	1	fveq2i	$$⊢\left|A\cup \left(B\setminus A\right)\right|=\left|A\cup B\right|$$
3		diffi	$$⊢B\in \mathrm{Fin}\to B\setminus A\in \mathrm{Fin}$$
4		disjdif	$$⊢A\cap \left(B\setminus A\right)=\varnothing$$
5		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|$$
6	4 5	mp3an3	$$⊢\left(A\in \mathrm{Fin}\wedge B\setminus A\in \mathrm{Fin}\right)\to \left|A\cup \left(B\setminus A\right)\right|=\left|A\right|+\left|B\setminus A\right|$$
7	3 6	sylan2	$$⊢\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|$$
8	2 7	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|$$
9	3	adantl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to B\setminus A\in \mathrm{Fin}$$
10		hashcl	$$⊢B\setminus A\in \mathrm{Fin}\to \left|B\setminus A\right|\in {\mathbb{N}}_0$$
11	9 10	syl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\setminus A\right|\in {\mathbb{N}}_0$$
12	11	nn0red	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\setminus A\right|\in ℝ$$
13		hashcl	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in {\mathbb{N}}_0$$
14	13	adantl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\right|\in {\mathbb{N}}_0$$
15	14	nn0red	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\right|\in ℝ$$
16		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
17	16	adantr	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\right|\in {\mathbb{N}}_0$$
18	17	nn0red	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\right|\in ℝ$$
19		simpr	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to B\in \mathrm{Fin}$$
20		difss	$$⊢B\setminus A\subseteq B$$
21		ssdomg	$$⊢B\in \mathrm{Fin}\to \left(B\setminus A\subseteq B\to \left(B\setminus A\right)\preccurlyeq B\right)$$
22	19 20 21	mpisyl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(B\setminus A\right)\preccurlyeq B$$
23		hashdom	$$⊢\left(B\setminus A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|B\setminus A\right|\le \left|B\right|\leftrightarrow \left(B\setminus A\right)\preccurlyeq B\right)$$
24	9 23	sylancom	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|B\setminus A\right|\le \left|B\right|\leftrightarrow \left(B\setminus A\right)\preccurlyeq B\right)$$
25	22 24	mpbird	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\setminus A\right|\le \left|B\right|$$
26	12 15 18 25	leadd2dd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\right|+\left|B\setminus A\right|\le \left|A\right|+\left|B\right|$$
27	8 26	eqbrtrd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|A\cup B\right|\le \left|A\right|+\left|B\right|$$