# Metamath Proof Explorer

## Theorem rnmptbdlem

Description: Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses rnmptbdlem.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
rnmptbdlem.y ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
rnmptbdlem.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
Assertion rnmptbdlem ${⊢}{\phi }\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)$

### Proof

Step Hyp Ref Expression
1 rnmptbdlem.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 rnmptbdlem.y ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 rnmptbdlem.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
4 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}ℝ$
5 nfra1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
6 4 5 nfrex ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
7 1 6 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)$
8 simpr ${⊢}\left({\phi }\wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
9 7 8 rnmptbdd ${⊢}\left({\phi }\wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}$
10 9 ex ${⊢}{\phi }\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)$
11 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)$
12 11 nfrn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({x}\in {A}⟼{B}\right)$
13 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\le {y}$
14 12 13 nfralw ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}$
15 1 14 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)$
16 breq1 ${⊢}{z}={B}\to \left({z}\le {y}↔{B}\le {y}\right)$
17 simplr ${⊢}\left(\left({\phi }\wedge \forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)\wedge {x}\in {A}\right)\to \forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}$
18 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
19 simpr ${⊢}\left(\left({\phi }\wedge \forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)\wedge {x}\in {A}\right)\to {x}\in {A}$
20 3 adantlr ${⊢}\left(\left({\phi }\wedge \forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)\wedge {x}\in {A}\right)\to {B}\in {V}$
21 18 19 20 elrnmpt1d ${⊢}\left(\left({\phi }\wedge \forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)\wedge {x}\in {A}\right)\to {B}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)$
22 16 17 21 rspcdva ${⊢}\left(\left({\phi }\wedge \forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)\wedge {x}\in {A}\right)\to {B}\le {y}$
23 15 22 ralrimia ${⊢}\left({\phi }\wedge \forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
24 23 ex ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)$
25 24 a1d ${⊢}{\phi }\to \left({y}\in ℝ\to \left(\forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\right)$
26 2 25 reximdai ${⊢}{\phi }\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)$
27 10 26 impbid ${⊢}{\phi }\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left({x}\in {A}⟼{B}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)$