This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐶 = ( 𝐴 ∪ 𝐵 )
hashunlei.a ⊢ ( 𝐴 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) ≤ 𝐾 )
hashunlei.b ⊢ ( 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐵 ) ≤ 𝑀 )
hashunlei.k ⊢ 𝐾 ∈ ℕ0
hashunlei.m ⊢ 𝑀 ∈ ℕ0
hashunlei.n ⊢ ( 𝐾 + 𝑀 ) = 𝑁
Assertion hashunlei ( 𝐶 ∈ Fin ∧ ( ♯ ‘ 𝐶 ) ≤ 𝑁 )

Proof

Step Hyp Ref Expression
1 hashunlei.c ⊢ 𝐶 = ( 𝐴 ∪ 𝐵 )
2 hashunlei.a ⊢ ( 𝐴 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) ≤ 𝐾 )
3 hashunlei.b ⊢ ( 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐵 ) ≤ 𝑀 )
4 hashunlei.k ⊢ 𝐾 ∈ ℕ0
5 hashunlei.m ⊢ 𝑀 ∈ ℕ0
6 hashunlei.n ⊢ ( 𝐾 + 𝑀 ) = 𝑁
7 2 simpli ⊢ 𝐴 ∈ Fin
8 3 simpli ⊢ 𝐵 ∈ Fin
9 unfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
10 7 8 9 mp2an ⊢ ( 𝐴 ∪ 𝐵 ) ∈ Fin
11 1 10 eqeltri ⊢ 𝐶 ∈ Fin
12 1 fveq2i ⊢ ( ♯ ‘ 𝐶 ) = ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) )
13 hashun2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
14 7 8 13 mp2an ⊢ ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) )
15 12 14 eqbrtri ⊢ ( ♯ ‘ 𝐶 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) )
16 2 simpri ⊢ ( ♯ ‘ 𝐴 ) ≤ 𝐾
17 3 simpri ⊢ ( ♯ ‘ 𝐵 ) ≤ 𝑀
18 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
19 7 18 ax-mp ⊢ ( ♯ ‘ 𝐴 ) ∈ ℕ0
20 19 nn0rei ⊢ ( ♯ ‘ 𝐴 ) ∈ ℝ
21 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
22 8 21 ax-mp ⊢ ( ♯ ‘ 𝐵 ) ∈ ℕ0
23 22 nn0rei ⊢ ( ♯ ‘ 𝐵 ) ∈ ℝ
24 4 nn0rei ⊢ 𝐾 ∈ ℝ
25 5 nn0rei ⊢ 𝑀 ∈ ℝ
26 20 23 24 25 le2addi ⊢ ( ( ( ♯ ‘ 𝐴 ) ≤ 𝐾 ∧ ( ♯ ‘ 𝐵 ) ≤ 𝑀 ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ≤ ( 𝐾 + 𝑀 ) )
27 16 17 26 mp2an ⊢ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ≤ ( 𝐾 + 𝑀 )
28 27 6 breqtri ⊢ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ≤ 𝑁
29 hashcl ⊢ ( 𝐶 ∈ Fin → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
30 11 29 ax-mp ⊢ ( ♯ ‘ 𝐶 ) ∈ ℕ0
31 30 nn0rei ⊢ ( ♯ ‘ 𝐶 ) ∈ ℝ
32 20 23 readdcli ⊢ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℝ
33 24 25 readdcli ⊢ ( 𝐾 + 𝑀 ) ∈ ℝ
34 6 33 eqeltrri ⊢ 𝑁 ∈ ℝ
35 31 32 34 letri ⊢ ( ( ( ♯ ‘ 𝐶 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∧ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ≤ 𝑁 ) → ( ♯ ‘ 𝐶 ) ≤ 𝑁 )
36 15 28 35 mp2an ⊢ ( ♯ ‘ 𝐶 ) ≤ 𝑁
37 11 36 pm3.2i ⊢ ( 𝐶 ∈ Fin ∧ ( ♯ ‘ 𝐶 ) ≤ 𝑁 )