Metamath Proof Explorer

Theorem hashsslei

Description: Get an upper bound on a concretely specified finite set. Transfer boundedness to a subset. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses hashsslei.b 
|- B C_ A
hashsslei.a 
|- ( A e. Fin /\ ( # ` A ) <_ N )
hashsslei.n 
|- N e. NN0
Assertion hashsslei 
|- ( B e. Fin /\ ( # ` B ) <_ N )

Proof

Step Hyp Ref Expression
1 hashsslei.b 
 |-  B C_ A
2 hashsslei.a 
 |-  ( A e. Fin /\ ( # ` A ) <_ N )
3 hashsslei.n 
 |-  N e. NN0
4 2 simpli 
 |-  A e. Fin
5 ssfi 
 |-  ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
6 4 1 5 mp2an 
 |-  B e. Fin
7 ssdomg 
 |-  ( A e. Fin -> ( B C_ A -> B ~<_ A ) )
8 4 1 7 mp2 
 |-  B ~<_ A
9 hashdom 
 |-  ( ( B e. Fin /\ A e. Fin ) -> ( ( # ` B ) <_ ( # ` A ) <-> B ~<_ A ) )
10 6 4 9 mp2an 
 |-  ( ( # ` B ) <_ ( # ` A ) <-> B ~<_ A )
11 8 10 mpbir 
 |-  ( # ` B ) <_ ( # ` A )
12 2 simpri 
 |-  ( # ` A ) <_ N
13 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
14 6 13 ax-mp 
 |-  ( # ` B ) e. NN0
15 14 nn0rei 
 |-  ( # ` B ) e. RR
16 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
17 4 16 ax-mp 
 |-  ( # ` A ) e. NN0
18 17 nn0rei 
 |-  ( # ` A ) e. RR
19 3 nn0rei 
 |-  N e. RR
20 15 18 19 letri 
 |-  ( ( ( # ` B ) <_ ( # ` A ) /\ ( # ` A ) <_ N ) -> ( # ` B ) <_ N )
21 11 12 20 mp2an 
 |-  ( # ` B ) <_ N
22 6 21 pm3.2i 
 |-  ( B e. Fin /\ ( # ` B ) <_ N )