# Metamath Proof Explorer

## Theorem nninfnub

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

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

### Proof

Step Hyp Ref Expression
1 eq0 ${⊢}\left\{{x}\in {A}|{B}<{x}\right\}=\varnothing ↔\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in \left\{{x}\in {A}|{B}<{x}\right\}$
2 breq2 ${⊢}{x}={y}\to \left({B}<{x}↔{B}<{y}\right)$
3 2 elrab ${⊢}{y}\in \left\{{x}\in {A}|{B}<{x}\right\}↔\left({y}\in {A}\wedge {B}<{y}\right)$
4 3 notbii ${⊢}¬{y}\in \left\{{x}\in {A}|{B}<{x}\right\}↔¬\left({y}\in {A}\wedge {B}<{y}\right)$
5 imnan ${⊢}\left({y}\in {A}\to ¬{B}<{y}\right)↔¬\left({y}\in {A}\wedge {B}<{y}\right)$
6 4 5 sylbb2 ${⊢}¬{y}\in \left\{{x}\in {A}|{B}<{x}\right\}\to \left({y}\in {A}\to ¬{B}<{y}\right)$
7 6 alimi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in \left\{{x}\in {A}|{B}<{x}\right\}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to ¬{B}<{y}\right)$
8 df-ral ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{y}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to ¬{B}<{y}\right)$
9 7 8 sylibr ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in \left\{{x}\in {A}|{B}<{x}\right\}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{y}$
10 ssel2 ${⊢}\left({A}\subseteq ℕ\wedge {y}\in {A}\right)\to {y}\in ℕ$
11 10 nnred ${⊢}\left({A}\subseteq ℕ\wedge {y}\in {A}\right)\to {y}\in ℝ$
12 11 adantlr ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\to {y}\in ℝ$
13 nnre ${⊢}{B}\in ℕ\to {B}\in ℝ$
14 13 ad2antlr ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\to {B}\in ℝ$
15 lenlt ${⊢}\left({y}\in ℝ\wedge {B}\in ℝ\right)\to \left({y}\le {B}↔¬{B}<{y}\right)$
16 15 biimprd ${⊢}\left({y}\in ℝ\wedge {B}\in ℝ\right)\to \left(¬{B}<{y}\to {y}\le {B}\right)$
17 12 14 16 syl2anc ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\to \left(¬{B}<{y}\to {y}\le {B}\right)$
18 17 ralimdva ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{y}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right)$
19 fzfi ${⊢}\left(0\dots {B}\right)\in \mathrm{Fin}$
20 10 nnnn0d ${⊢}\left({A}\subseteq ℕ\wedge {y}\in {A}\right)\to {y}\in {ℕ}_{0}$
21 20 adantlr ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\to {y}\in {ℕ}_{0}$
22 21 adantr ${⊢}\left(\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\wedge {y}\le {B}\right)\to {y}\in {ℕ}_{0}$
23 nnnn0 ${⊢}{B}\in ℕ\to {B}\in {ℕ}_{0}$
24 23 ad3antlr ${⊢}\left(\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\wedge {y}\le {B}\right)\to {B}\in {ℕ}_{0}$
25 simpr ${⊢}\left(\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\wedge {y}\le {B}\right)\to {y}\le {B}$
26 22 24 25 3jca ${⊢}\left(\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\wedge {y}\le {B}\right)\to \left({y}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {y}\le {B}\right)$
27 26 ex ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\to \left({y}\le {B}\to \left({y}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {y}\le {B}\right)\right)$
28 elfz2nn0 ${⊢}{y}\in \left(0\dots {B}\right)↔\left({y}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {y}\le {B}\right)$
29 27 28 syl6ibr ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge {y}\in {A}\right)\to \left({y}\le {B}\to {y}\in \left(0\dots {B}\right)\right)$
30 29 ralimdva ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {B}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left(0\dots {B}\right)\right)$
31 30 imp ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left(0\dots {B}\right)$
32 dfss3 ${⊢}{A}\subseteq \left(0\dots {B}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left(0\dots {B}\right)$
33 31 32 sylibr ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right)\to {A}\subseteq \left(0\dots {B}\right)$
34 ssfi ${⊢}\left(\left(0\dots {B}\right)\in \mathrm{Fin}\wedge {A}\subseteq \left(0\dots {B}\right)\right)\to {A}\in \mathrm{Fin}$
35 19 33 34 sylancr ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right)\to {A}\in \mathrm{Fin}$
36 35 ex ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {B}\to {A}\in \mathrm{Fin}\right)$
37 18 36 syld ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}<{y}\to {A}\in \mathrm{Fin}\right)$
38 9 37 syl5 ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in \left\{{x}\in {A}|{B}<{x}\right\}\to {A}\in \mathrm{Fin}\right)$
39 1 38 syl5bi ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left(\left\{{x}\in {A}|{B}<{x}\right\}=\varnothing \to {A}\in \mathrm{Fin}\right)$
40 39 necon3bd ${⊢}\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\to \left(¬{A}\in \mathrm{Fin}\to \left\{{x}\in {A}|{B}<{x}\right\}\ne \varnothing \right)$
41 40 imp ${⊢}\left(\left({A}\subseteq ℕ\wedge {B}\in ℕ\right)\wedge ¬{A}\in \mathrm{Fin}\right)\to \left\{{x}\in {A}|{B}<{x}\right\}\ne \varnothing$
42 41 an32s ${⊢}\left(\left({A}\subseteq ℕ\wedge ¬{A}\in \mathrm{Fin}\right)\wedge {B}\in ℕ\right)\to \left\{{x}\in {A}|{B}<{x}\right\}\ne \varnothing$
43 42 3impa ${⊢}\left({A}\subseteq ℕ\wedge ¬{A}\in \mathrm{Fin}\wedge {B}\in ℕ\right)\to \left\{{x}\in {A}|{B}<{x}\right\}\ne \varnothing$