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 ⊢ A ∈ V ∧ B ∈ ℕ 0 ∧ A ≤ B → A ∈ Fin

Proof

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