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

Metamath Proof Explorer

Theorem hashbnd

Description: If A has size bounded by an integer B , then A is finite. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Assertion hashbnd 
|- ( ( A e. V /\ B e. NN0 /\ ( # ` A ) <_ B ) -> A e. Fin )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( B e. NN0 -> B e. RR )
2 ltpnf 
 |-  ( B e. RR -> B < +oo )
3 rexr 
 |-  ( B e. RR -> B e. RR* )
4 pnfxr 
 |-  +oo e. RR*
5 xrltnle 
 |-  ( ( B e. RR* /\ +oo e. RR* ) -> ( B < +oo <-> -. +oo <_ B ) )
6 3 4 5 sylancl 
 |-  ( B e. RR -> ( B < +oo <-> -. +oo <_ B ) )
7 2 6 mpbid 
 |-  ( B e. RR -> -. +oo <_ B )
8 1 7 syl 
 |-  ( B e. NN0 -> -. +oo <_ B )
9 hashinf 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
10 9 breq1d 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( ( # ` A ) <_ B <-> +oo <_ B ) )
11 10 notbid 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( -. ( # ` A ) <_ B <-> -. +oo <_ B ) )
12 8 11 syl5ibrcom 
 |-  ( B e. NN0 -> ( ( A e. V /\ -. A e. Fin ) -> -. ( # ` A ) <_ B ) )
13 12 expdimp 
 |-  ( ( B e. NN0 /\ A e. V ) -> ( -. A e. Fin -> -. ( # ` A ) <_ B ) )
14 13 ancoms 
 |-  ( ( A e. V /\ B e. NN0 ) -> ( -. A e. Fin -> -. ( # ` A ) <_ B ) )
15 14 con4d 
 |-  ( ( A e. V /\ B e. NN0 ) -> ( ( # ` A ) <_ B -> A e. Fin ) )
16 15 3impia 
 |-  ( ( A e. V /\ B e. NN0 /\ ( # ` A ) <_ B ) -> A e. Fin )