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 ⊢Ⅎ_tF
rfcnpre4.2 ⊢K=topGen⁡ran⁡.
rfcnpre4.3 ⊢T=⋃J
rfcnpre4.4 ⊢A=t∈T|F⁡t≤B
rfcnpre4.5 ⊢φ→B∈ℝ
rfcnpre4.6 ⊢φ→F∈JCnK
Assertion rfcnpre4 ⊢φ→A∈Clsd⁡J

Proof

Step Hyp Ref Expression
1 rfcnpre4.1 ⊢Ⅎ_tF
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∈JCnK
7 eqid ⊢JCnK=JCnK
8 2 3 7 6 fcnre ⊢φ→F:T⟶ℝ
9 ffn ⊢F:T⟶ℝ→FFnT
10 elpreima ⊢FFnT→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 ffvelcdmda ⊢φ∧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 ⊢Ⅎ_ts
31 nfcv ⊢Ⅎ_tT
32 1 30 nffv ⊢Ⅎ_tF⁡s
33 nfcv ⊢Ⅎ_t≤
34 nfcv ⊢Ⅎ_tB
35 32 33 34 nfbr ⊢ℲtF⁡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∈JCnK∧−∞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