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 ∧ ( ♯ ‘ 𝐶 ) ≤ 𝑁 )