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 ( ( 𝐴𝑉𝐵 ∈ ℕ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 )