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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ≤ 𝐵 ) → 𝐴 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℝ )
2		ltpnf	⊢ ( 𝐵 ∈ ℝ → 𝐵 < +∞ )
3		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
4		pnfxr	⊢ +∞ ∈ ℝ*
5		xrltnle	⊢ ( ( 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵 ) )
6	3 4 5	sylancl	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵 ) )
7	2 6	mpbid	⊢ ( 𝐵 ∈ ℝ → ¬ +∞ ≤ 𝐵 )
8	1 7	syl	⊢ ( 𝐵 ∈ ℕ0 → ¬ +∞ ≤ 𝐵 )
9		hashinf	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
10	9	breq1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ 𝐵 ↔ +∞ ≤ 𝐵 ) )
11	10	notbid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ¬ ( ♯ ‘ 𝐴 ) ≤ 𝐵 ↔ ¬ +∞ ≤ 𝐵 ) )
12	8 11	syl5ibrcom	⊢ ( 𝐵 ∈ ℕ0 → ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ¬ ( ♯ ‘ 𝐴 ) ≤ 𝐵 ) )
13	12	expdimp	⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐴 ∈ 𝑉 ) → ( ¬ 𝐴 ∈ Fin → ¬ ( ♯ ‘ 𝐴 ) ≤ 𝐵 ) )
14	13	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ℕ0 ) → ( ¬ 𝐴 ∈ Fin → ¬ ( ♯ ‘ 𝐴 ) ≤ 𝐵 ) )
15	14	con4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) ≤ 𝐵 → 𝐴 ∈ Fin ) )
16	15	3impia	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ≤ 𝐵 ) → 𝐴 ∈ Fin )