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 | |
|
rfcnpre2.2 | |
||
rfcnpre2.3 | |
||
rfcnpre2.4 | |
||
rfcnpre2.5 | |
||
rfcnpre2.6 | |
||
rfcnpre2.7 | |
||
rfcnpre2.8 | |
||
Assertion | rfcnpre2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rfcnpre2.1 | |
|
2 | rfcnpre2.2 | |
|
3 | rfcnpre2.3 | |
|
4 | rfcnpre2.4 | |
|
5 | rfcnpre2.5 | |
|
6 | rfcnpre2.6 | |
|
7 | rfcnpre2.7 | |
|
8 | rfcnpre2.8 | |
|
9 | 2 | nfcnv | |
10 | nfcv | |
|
11 | nfcv | |
|
12 | 10 11 1 | nfov | |
13 | 9 12 | nfima | |
14 | nfrab1 | |
|
15 | eqid | |
|
16 | 4 5 15 8 | fcnre | |
17 | 16 | ffvelrnda | |
18 | elioomnf | |
|
19 | 7 18 | syl | |
20 | 19 | baibd | |
21 | 17 20 | syldan | |
22 | 21 | pm5.32da | |
23 | ffn | |
|
24 | elpreima | |
|
25 | 16 23 24 | 3syl | |
26 | rabid | |
|
27 | 26 | a1i | |
28 | 22 25 27 | 3bitr4d | |
29 | 3 13 14 28 | eqrd | |
30 | 29 6 | eqtr4di | |
31 | iooretop | |
|
32 | 31 | a1i | |
33 | 32 4 | eleqtrrdi | |
34 | cnima | |
|
35 | 8 33 34 | syl2anc | |
36 | 30 35 | eqeltrrd | |