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	$$⊢\left(A\in V\wedge B\in {\mathbb{N}}_0\wedge \left|A\right|\le B\right)\to A\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢B\in {\mathbb{N}}_0\to B\in ℝ$$
2		ltpnf	$$⊢B\in ℝ\to B<\mathrm{+\infty }$$
3		rexr	$$⊢B\in ℝ\to B\in {ℝ}^{*}$$
4		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
5		xrltnle	$$⊢\left(B\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(B<\mathrm{+\infty }\leftrightarrow \neg \mathrm{+\infty }\le B\right)$$
6	3 4 5	sylancl	$$⊢B\in ℝ\to \left(B<\mathrm{+\infty }\leftrightarrow \neg \mathrm{+\infty }\le B\right)$$
7	2 6	mpbid	$$⊢B\in ℝ\to \neg \mathrm{+\infty }\le B$$
8	1 7	syl	$$⊢B\in {\mathbb{N}}_0\to \neg \mathrm{+\infty }\le B$$
9		hashinf	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left|A\right|=\mathrm{+\infty }$$
10	9	breq1d	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left(\left|A\right|\le B\leftrightarrow \mathrm{+\infty }\le B\right)$$
11	10	notbid	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left(\neg \left|A\right|\le B\leftrightarrow \neg \mathrm{+\infty }\le B\right)$$
12	8 11	syl5ibrcom	$$⊢B\in {\mathbb{N}}_0\to \left(\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \neg \left|A\right|\le B\right)$$
13	12	expdimp	$$⊢\left(B\in {\mathbb{N}}_0\wedge A\in V\right)\to \left(\neg A\in \mathrm{Fin}\to \neg \left|A\right|\le B\right)$$
14	13	ancoms	$$⊢\left(A\in V\wedge B\in {\mathbb{N}}_0\right)\to \left(\neg A\in \mathrm{Fin}\to \neg \left|A\right|\le B\right)$$
15	14	con4d	$$⊢\left(A\in V\wedge B\in {\mathbb{N}}_0\right)\to \left(\left|A\right|\le B\to A\in \mathrm{Fin}\right)$$
16	15	3impia	$$⊢\left(A\in V\wedge B\in {\mathbb{N}}_0\wedge \left|A\right|\le B\right)\to A\in \mathrm{Fin}$$