Theorem hashunlei

Description: Get an upper bound on a concretely specified finite set. Induction step: union of two finite bounded sets. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	hashunlei.c	$$⊢C=A\cup B$$
	hashunlei.a	$$⊢\left(A\in \mathrm{Fin}\wedge \left|A\right|\le K\right)$$
	hashunlei.b	$$⊢\left(B\in \mathrm{Fin}\wedge \left|B\right|\le M\right)$$
	hashunlei.k	$$⊢K\in {\mathbb{N}}_0$$
	hashunlei.m	$$⊢M\in {\mathbb{N}}_0$$
	hashunlei.n	$$⊢K+M=N$$
Assertion	hashunlei	$$⊢\left(C\in \mathrm{Fin}\wedge \left|C\right|\le N\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashunlei.c	$$⊢C=A\cup B$$
2		hashunlei.a	$$⊢\left(A\in \mathrm{Fin}\wedge \left|A\right|\le K\right)$$
3		hashunlei.b	$$⊢\left(B\in \mathrm{Fin}\wedge \left|B\right|\le M\right)$$
4		hashunlei.k	$$⊢K\in {\mathbb{N}}_0$$
5		hashunlei.m	$$⊢M\in {\mathbb{N}}_0$$
6		hashunlei.n	$$⊢K+M=N$$
7	2	simpli	$$⊢A\in \mathrm{Fin}$$
8	3	simpli	$$⊢B\in \mathrm{Fin}$$
9		unfi	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\cup B\in \mathrm{Fin}$$
10	7 8 9	mp2an	$$⊢A\cup B\in \mathrm{Fin}$$
11	1 10	eqeltri	$$⊢C\in \mathrm{Fin}$$
12	1	fveq2i	$$⊢\left|C\right|=\left|A\cup B\right|$$
13		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|$$
14	7 8 13	mp2an	$$⊢\left|A\cup B\right|\le \left|A\right|+\left|B\right|$$
15	12 14	eqbrtri	$$⊢\left|C\right|\le \left|A\right|+\left|B\right|$$
16	2	simpri	$$⊢\left|A\right|\le K$$
17	3	simpri	$$⊢\left|B\right|\le M$$
18		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
19	7 18	ax-mp	$$⊢\left|A\right|\in {\mathbb{N}}_0$$
20	19	nn0rei	$$⊢\left|A\right|\in ℝ$$
21		hashcl	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in {\mathbb{N}}_0$$
22	8 21	ax-mp	$$⊢\left|B\right|\in {\mathbb{N}}_0$$
23	22	nn0rei	$$⊢\left|B\right|\in ℝ$$
24	4	nn0rei	$$⊢K\in ℝ$$
25	5	nn0rei	$$⊢M\in ℝ$$
26	20 23 24 25	le2addi	$$⊢\left(\left|A\right|\le K\wedge \left|B\right|\le M\right)\to \left|A\right|+\left|B\right|\le K+M$$
27	16 17 26	mp2an	$$⊢\left|A\right|+\left|B\right|\le K+M$$
28	27 6	breqtri	$$⊢\left|A\right|+\left|B\right|\le N$$
29		hashcl	$$⊢C\in \mathrm{Fin}\to \left|C\right|\in {\mathbb{N}}_0$$
30	11 29	ax-mp	$$⊢\left|C\right|\in {\mathbb{N}}_0$$
31	30	nn0rei	$$⊢\left|C\right|\in ℝ$$
32	20 23	readdcli	$$⊢\left|A\right|+\left|B\right|\in ℝ$$
33	24 25	readdcli	$$⊢K+M\in ℝ$$
34	6 33	eqeltrri	$$⊢N\in ℝ$$
35	31 32 34	letri	$$⊢\left(\left|C\right|\le \left|A\right|+\left|B\right|\wedge \left|A\right|+\left|B\right|\le N\right)\to \left|C\right|\le N$$
36	15 28 35	mp2an	$$⊢\left|C\right|\le N$$
37	11 36	pm3.2i	$$⊢\left(C\in \mathrm{Fin}\wedge \left|C\right|\le N\right)$$