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 _ x B
rfcnpre2.2 _ x F
rfcnpre2.3 x φ
rfcnpre2.4 K = topGen ran .
rfcnpre2.5 X = J
rfcnpre2.6 A = x X | F x < B
rfcnpre2.7 φ B *
rfcnpre2.8 φ F J Cn K
Assertion rfcnpre2 φ A J

Proof

Step Hyp Ref Expression
1 rfcnpre2.1 _ x B
2 rfcnpre2.2 _ x F
3 rfcnpre2.3 x φ
4 rfcnpre2.4 K = topGen ran .
5 rfcnpre2.5 X = J
6 rfcnpre2.6 A = x X | F x < B
7 rfcnpre2.7 φ B *
8 rfcnpre2.8 φ F J Cn K
9 2 nfcnv _ x F -1
10 nfcv _ x −∞
11 nfcv _ x .
12 10 11 1 nfov _ x −∞ B
13 9 12 nfima _ x F -1 −∞ B
14 nfrab1 _ x x X | F x < B
15 eqid J Cn K = J Cn K
16 4 5 15 8 fcnre φ F : X
17 16 ffvelrnda φ x X F x
18 elioomnf B * F x −∞ B F x F x < B
19 7 18 syl φ F x −∞ B F x F x < B
20 19 baibd φ F x F x −∞ B F x < B
21 17 20 syldan φ x X F x −∞ B F x < B
22 21 pm5.32da φ x X F x −∞ B x X F x < B
23 ffn F : X F Fn X
24 elpreima F Fn X x F -1 −∞ B x X F x −∞ B
25 16 23 24 3syl φ x F -1 −∞ B x X F x −∞ B
26 rabid x x X | F x < B x X F x < B
27 26 a1i φ x x X | F x < B x X F x < B
28 22 25 27 3bitr4d φ x F -1 −∞ B x x X | F x < B
29 3 13 14 28 eqrd φ F -1 −∞ B = x X | F x < B
30 29 6 syl6eqr φ F -1 −∞ B = A
31 iooretop −∞ B topGen ran .
32 31 a1i φ −∞ B topGen ran .
33 32 4 eleqtrrdi φ −∞ B K
34 cnima F J Cn K −∞ B K F -1 −∞ B J
35 8 33 34 syl2anc φ F -1 −∞ B J
36 30 35 eqeltrrd φ A J