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 u. B )
hashunlei.a 
|- ( A e. Fin /\ ( # ` A ) <_ K )
hashunlei.b 
|- ( B e. Fin /\ ( # ` B ) <_ M )
hashunlei.k 
|- K e. NN0
hashunlei.m 
|- M e. NN0
hashunlei.n 
|- ( K + M ) = N
Assertion hashunlei 
|- ( C e. Fin /\ ( # ` C ) <_ N )

Proof

Step Hyp Ref Expression
1 hashunlei.c 
 |-  C = ( A u. B )
2 hashunlei.a 
 |-  ( A e. Fin /\ ( # ` A ) <_ K )
3 hashunlei.b 
 |-  ( B e. Fin /\ ( # ` B ) <_ M )
4 hashunlei.k 
 |-  K e. NN0
5 hashunlei.m 
 |-  M e. NN0
6 hashunlei.n 
 |-  ( K + M ) = N
7 2 simpli 
 |-  A e. Fin
8 3 simpli 
 |-  B e. Fin
9 unfi 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
10 7 8 9 mp2an 
 |-  ( A u. B ) e. Fin
11 1 10 eqeltri 
 |-  C e. Fin
12 1 fveq2i 
 |-  ( # ` C ) = ( # ` ( A u. B ) )
13 hashun2 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) <_ ( ( # ` A ) + ( # ` B ) ) )
14 7 8 13 mp2an 
 |-  ( # ` ( A u. B ) ) <_ ( ( # ` A ) + ( # ` B ) )
15 12 14 eqbrtri 
 |-  ( # ` C ) <_ ( ( # ` A ) + ( # ` B ) )
16 2 simpri 
 |-  ( # ` A ) <_ K
17 3 simpri 
 |-  ( # ` B ) <_ M
18 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
19 7 18 ax-mp 
 |-  ( # ` A ) e. NN0
20 19 nn0rei 
 |-  ( # ` A ) e. RR
21 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
22 8 21 ax-mp 
 |-  ( # ` B ) e. NN0
23 22 nn0rei 
 |-  ( # ` B ) e. RR
24 4 nn0rei 
 |-  K e. RR
25 5 nn0rei 
 |-  M e. RR
26 20 23 24 25 le2addi 
 |-  ( ( ( # ` A ) <_ K /\ ( # ` B ) <_ M ) -> ( ( # ` A ) + ( # ` B ) ) <_ ( K + M ) )
27 16 17 26 mp2an 
 |-  ( ( # ` A ) + ( # ` B ) ) <_ ( K + M )
28 27 6 breqtri 
 |-  ( ( # ` A ) + ( # ` B ) ) <_ N
29 hashcl 
 |-  ( C e. Fin -> ( # ` C ) e. NN0 )
30 11 29 ax-mp 
 |-  ( # ` C ) e. NN0
31 30 nn0rei 
 |-  ( # ` C ) e. RR
32 20 23 readdcli 
 |-  ( ( # ` A ) + ( # ` B ) ) e. RR
33 24 25 readdcli 
 |-  ( K + M ) e. RR
34 6 33 eqeltrri 
 |-  N e. RR
35 31 32 34 letri 
 |-  ( ( ( # ` C ) <_ ( ( # ` A ) + ( # ` B ) ) /\ ( ( # ` A ) + ( # ` B ) ) <_ N ) -> ( # ` C ) <_ N )
36 15 28 35 mp2an 
 |-  ( # ` C ) <_ N
37 11 36 pm3.2i 
 |-  ( C e. Fin /\ ( # ` C ) <_ N )