Metamath Proof Explorer


Theorem rfcnpre4

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

Ref Expression
Hypotheses rfcnpre4.1 _ t F
rfcnpre4.2 K = topGen ran .
rfcnpre4.3 T = J
rfcnpre4.4 A = t T | F t B
rfcnpre4.5 φ B
rfcnpre4.6 φ F J Cn K
Assertion rfcnpre4 φ A Clsd J

Proof

Step Hyp Ref Expression
1 rfcnpre4.1 _ t F
2 rfcnpre4.2 K = topGen ran .
3 rfcnpre4.3 T = J
4 rfcnpre4.4 A = t T | F t B
5 rfcnpre4.5 φ B
6 rfcnpre4.6 φ F J Cn K
7 eqid J Cn K = J Cn K
8 2 3 7 6 fcnre φ F : T
9 ffn F : T F Fn T
10 elpreima F Fn T s F -1 −∞ B s T F s −∞ B
11 8 9 10 3syl φ s F -1 −∞ B s T F s −∞ B
12 mnfxr −∞ *
13 5 rexrd φ B *
14 13 adantr φ s T B *
15 elioc1 −∞ * B * F s −∞ B F s * −∞ < F s F s B
16 12 14 15 sylancr φ s T F s −∞ B F s * −∞ < F s F s B
17 simpr3 φ s T F s * −∞ < F s F s B F s B
18 8 ffvelrnda φ s T F s
19 18 rexrd φ s T F s *
20 19 adantr φ s T F s B F s *
21 18 adantr φ s T F s B F s
22 mnflt F s −∞ < F s
23 21 22 syl φ s T F s B −∞ < F s
24 simpr φ s T F s B F s B
25 20 23 24 3jca φ s T F s B F s * −∞ < F s F s B
26 17 25 impbida φ s T F s * −∞ < F s F s B F s B
27 16 26 bitrd φ s T F s −∞ B F s B
28 27 pm5.32da φ s T F s −∞ B s T F s B
29 11 28 bitrd φ s F -1 −∞ B s T F s B
30 nfcv _ t s
31 nfcv _ t T
32 1 30 nffv _ t F s
33 nfcv _ t
34 nfcv _ t B
35 32 33 34 nfbr t F s B
36 fveq2 t = s F t = F s
37 36 breq1d t = s F t B F s B
38 30 31 35 37 elrabf s t T | F t B s T F s B
39 29 38 bitr4di φ s F -1 −∞ B s t T | F t B
40 39 eqrdv φ F -1 −∞ B = t T | F t B
41 40 4 eqtr4di φ F -1 −∞ B = A
42 iocmnfcld B −∞ B Clsd topGen ran .
43 5 42 syl φ −∞ B Clsd topGen ran .
44 2 fveq2i Clsd K = Clsd topGen ran .
45 43 44 eleqtrrdi φ −∞ B Clsd K
46 cnclima F J Cn K −∞ B Clsd K F -1 −∞ B Clsd J
47 6 45 46 syl2anc φ F -1 −∞ B Clsd J
48 41 47 eqeltrrd φ A Clsd J