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