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