# Metamath Proof Explorer

## 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 {ℕ}_{0}$
hashunlei.m ${⊢}{M}\in {ℕ}_{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 {ℕ}_{0}$
5 hashunlei.m ${⊢}{M}\in {ℕ}_{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 {ℕ}_{0}$
19 7 18 ax-mp ${⊢}\left|{A}\right|\in {ℕ}_{0}$
20 19 nn0rei ${⊢}\left|{A}\right|\in ℝ$
21 hashcl ${⊢}{B}\in \mathrm{Fin}\to \left|{B}\right|\in {ℕ}_{0}$
22 8 21 ax-mp ${⊢}\left|{B}\right|\in {ℕ}_{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 {ℕ}_{0}$
30 11 29 ax-mp ${⊢}\left|{C}\right|\in {ℕ}_{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)$