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 )