# Metamath Proof Explorer

## Theorem nnubfi

Description: A bounded above set of positive integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 28-Feb-2014)

Ref Expression
Assertion nnubfi ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left\{{x}\in {A}|{x}<{B}\right\}\in \mathrm{Fin}$

### Proof

Step Hyp Ref Expression
1 fzfi ${⊢}\left(0\dots {B}\right)\in \mathrm{Fin}$
2 ssel2 ${⊢}\left({A}\subseteq ℕ\wedge {x}\in {A}\right)\to {x}\in ℕ$
3 nnnn0 ${⊢}{x}\in ℕ\to {x}\in {ℕ}_{0}$
4 2 3 syl ${⊢}\left({A}\subseteq ℕ\wedge {x}\in {A}\right)\to {x}\in {ℕ}_{0}$
5 4 adantlr ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {x}\in {A}\right)\to {x}\in {ℕ}_{0}$
6 5 adantr ${⊢}\left(\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {x}\in {A}\right)\wedge {x}<{B}\right)\to {x}\in {ℕ}_{0}$
7 nnnn0 ${⊢}{B}\in ℕ\to {B}\in {ℕ}_{0}$
8 7 ad3antlr ${⊢}\left(\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {x}\in {A}\right)\wedge {x}<{B}\right)\to {B}\in {ℕ}_{0}$
9 nnre ${⊢}{x}\in ℕ\to {x}\in ℝ$
10 2 9 syl ${⊢}\left({A}\subseteq ℕ\wedge {x}\in {A}\right)\to {x}\in ℝ$
11 10 adantlr ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {x}\in {A}\right)\to {x}\in ℝ$
12 nnre ${⊢}{B}\in ℕ\to {B}\in ℝ$
13 12 ad2antlr ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {x}\in {A}\right)\to {B}\in ℝ$
14 ltle ${⊢}\left({x}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}<{B}\to {x}\le {B}\right)$
15 11 13 14 syl2anc ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {x}\in {A}\right)\to \left({x}<{B}\to {x}\le {B}\right)$
16 15 imp ${⊢}\left(\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {x}\in {A}\right)\wedge {x}<{B}\right)\to {x}\le {B}$
17 elfz2nn0 ${⊢}{x}\in \left(0\dots {B}\right)↔\left({x}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {x}\le {B}\right)$
18 6 8 16 17 syl3anbrc ${⊢}\left(\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {x}\in {A}\right)\wedge {x}<{B}\right)\to {x}\in \left(0\dots {B}\right)$
19 18 ex ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {x}\in {A}\right)\to \left({x}<{B}\to {x}\in \left(0\dots {B}\right)\right)$
20 19 ralrimiva ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to {x}\in \left(0\dots {B}\right)\right)$
21 rabss ${⊢}\left\{{x}\in {A}|{x}<{B}\right\}\subseteq \left(0\dots {B}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}<{B}\to {x}\in \left(0\dots {B}\right)\right)$
22 20 21 sylibr ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left\{{x}\in {A}|{x}<{B}\right\}\subseteq \left(0\dots {B}\right)$
23 ssfi ${⊢}\left(\left(0\dots {B}\right)\in \mathrm{Fin}\wedge \left\{{x}\in {A}|{x}<{B}\right\}\subseteq \left(0\dots {B}\right)\right)\to \left\{{x}\in {A}|{x}<{B}\right\}\in \mathrm{Fin}$
24 1 22 23 sylancr ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left\{{x}\in {A}|{x}<{B}\right\}\in \mathrm{Fin}$