# Metamath Proof Explorer

## Theorem rfcnpre2

Description: If F is a continuous function with respect to the standard topology, then the preimage A of the values smaller than a given extended real B , is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses rfcnpre2.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
rfcnpre2.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
rfcnpre2.3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
rfcnpre2.4 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
rfcnpre2.5 ${⊢}{X}=\bigcup {J}$
rfcnpre2.6 ${⊢}{A}=\left\{{x}\in {X}|{F}\left({x}\right)<{B}\right\}$
rfcnpre2.7 ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
rfcnpre2.8 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
Assertion rfcnpre2 ${⊢}{\phi }\to {A}\in {J}$

### Proof

Step Hyp Ref Expression
1 rfcnpre2.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
2 rfcnpre2.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
3 rfcnpre2.3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
4 rfcnpre2.4 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
5 rfcnpre2.5 ${⊢}{X}=\bigcup {J}$
6 rfcnpre2.6 ${⊢}{A}=\left\{{x}\in {X}|{F}\left({x}\right)<{B}\right\}$
7 rfcnpre2.7 ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
8 rfcnpre2.8 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
9 2 nfcnv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}$
10 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{-\infty }$
11 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(.\right)$
12 10 11 1 nfov ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty },{B}\right)$
13 9 12 nfima ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]$
14 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {X}|{F}\left({x}\right)<{B}\right\}$
15 eqid ${⊢}{J}\mathrm{Cn}{K}={J}\mathrm{Cn}{K}$
16 4 5 15 8 fcnre ${⊢}{\phi }\to {F}:{X}⟶ℝ$
17 16 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {F}\left({x}\right)\in ℝ$
18 elioomnf ${⊢}{B}\in {ℝ}^{*}\to \left({F}\left({x}\right)\in \left(\mathrm{-\infty },{B}\right)↔\left({F}\left({x}\right)\in ℝ\wedge {F}\left({x}\right)<{B}\right)\right)$
19 7 18 syl ${⊢}{\phi }\to \left({F}\left({x}\right)\in \left(\mathrm{-\infty },{B}\right)↔\left({F}\left({x}\right)\in ℝ\wedge {F}\left({x}\right)<{B}\right)\right)$
20 19 baibd ${⊢}\left({\phi }\wedge {F}\left({x}\right)\in ℝ\right)\to \left({F}\left({x}\right)\in \left(\mathrm{-\infty },{B}\right)↔{F}\left({x}\right)<{B}\right)$
21 17 20 syldan ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({F}\left({x}\right)\in \left(\mathrm{-\infty },{B}\right)↔{F}\left({x}\right)<{B}\right)$
22 21 pm5.32da ${⊢}{\phi }\to \left(\left({x}\in {X}\wedge {F}\left({x}\right)\in \left(\mathrm{-\infty },{B}\right)\right)↔\left({x}\in {X}\wedge {F}\left({x}\right)<{B}\right)\right)$
23 ffn ${⊢}{F}:{X}⟶ℝ\to {F}Fn{X}$
24 elpreima ${⊢}{F}Fn{X}\to \left({x}\in {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]↔\left({x}\in {X}\wedge {F}\left({x}\right)\in \left(\mathrm{-\infty },{B}\right)\right)\right)$
25 16 23 24 3syl ${⊢}{\phi }\to \left({x}\in {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]↔\left({x}\in {X}\wedge {F}\left({x}\right)\in \left(\mathrm{-\infty },{B}\right)\right)\right)$
26 rabid ${⊢}{x}\in \left\{{x}\in {X}|{F}\left({x}\right)<{B}\right\}↔\left({x}\in {X}\wedge {F}\left({x}\right)<{B}\right)$
27 26 a1i ${⊢}{\phi }\to \left({x}\in \left\{{x}\in {X}|{F}\left({x}\right)<{B}\right\}↔\left({x}\in {X}\wedge {F}\left({x}\right)<{B}\right)\right)$
28 22 25 27 3bitr4d ${⊢}{\phi }\to \left({x}\in {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]↔{x}\in \left\{{x}\in {X}|{F}\left({x}\right)<{B}\right\}\right)$
29 3 13 14 28 eqrd ${⊢}{\phi }\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]=\left\{{x}\in {X}|{F}\left({x}\right)<{B}\right\}$
30 29 6 syl6eqr ${⊢}{\phi }\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]={A}$
31 iooretop ${⊢}\left(\mathrm{-\infty },{B}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
32 31 a1i ${⊢}{\phi }\to \left(\mathrm{-\infty },{B}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
33 32 4 eleqtrrdi ${⊢}{\phi }\to \left(\mathrm{-\infty },{B}\right)\in {K}$
34 cnima ${⊢}\left({F}\in \left({J}\mathrm{Cn}{K}\right)\wedge \left(\mathrm{-\infty },{B}\right)\in {K}\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]\in {J}$
35 8 33 34 syl2anc ${⊢}{\phi }\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]\in {J}$
36 30 35 eqeltrrd ${⊢}{\phi }\to {A}\in {J}$