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 _xB
rfcnpre2.2 _xF
rfcnpre2.3 xφ
rfcnpre2.4 K=topGenran.
rfcnpre2.5 X=J
rfcnpre2.6 A=xX|Fx<B
rfcnpre2.7 φB*
rfcnpre2.8 φFJCnK
Assertion rfcnpre2 φAJ

Proof

Step Hyp Ref Expression
1 rfcnpre2.1 _xB
2 rfcnpre2.2 _xF
3 rfcnpre2.3 xφ
4 rfcnpre2.4 K=topGenran.
5 rfcnpre2.5 X=J
6 rfcnpre2.6 A=xX|Fx<B
7 rfcnpre2.7 φB*
8 rfcnpre2.8 φFJCnK
9 2 nfcnv _xF-1
10 nfcv _x−∞
11 nfcv _x.
12 10 11 1 nfov _x−∞B
13 9 12 nfima _xF-1−∞B
14 nfrab1 _xxX|Fx<B
15 eqid JCnK=JCnK
16 4 5 15 8 fcnre φF:X
17 16 ffvelrnda φxXFx
18 elioomnf B*Fx−∞BFxFx<B
19 7 18 syl φFx−∞BFxFx<B
20 19 baibd φFxFx−∞BFx<B
21 17 20 syldan φxXFx−∞BFx<B
22 21 pm5.32da φxXFx−∞BxXFx<B
23 ffn F:XFFnX
24 elpreima FFnXxF-1−∞BxXFx−∞B
25 16 23 24 3syl φxF-1−∞BxXFx−∞B
26 rabid xxX|Fx<BxXFx<B
27 26 a1i φxxX|Fx<BxXFx<B
28 22 25 27 3bitr4d φxF-1−∞BxxX|Fx<B
29 3 13 14 28 eqrd φF-1−∞B=xX|Fx<B
30 29 6 eqtr4di φF-1−∞B=A
31 iooretop −∞BtopGenran.
32 31 a1i φ−∞BtopGenran.
33 32 4 eleqtrrdi φ−∞BK
34 cnima FJCnK−∞BKF-1−∞BJ
35 8 33 34 syl2anc φF-1−∞BJ
36 30 35 eqeltrrd φAJ