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 𝑡 𝐹
rfcnpre4.2 𝐾 = ( topGen ‘ ran (,) )
rfcnpre4.3 𝑇 = 𝐽
rfcnpre4.4 𝐴 = { 𝑡𝑇 ∣ ( 𝐹𝑡 ) ≤ 𝐵 }
rfcnpre4.5 ( 𝜑𝐵 ∈ ℝ )
rfcnpre4.6 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion rfcnpre4 ( 𝜑𝐴 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 rfcnpre4.1 𝑡 𝐹
2 rfcnpre4.2 𝐾 = ( topGen ‘ ran (,) )
3 rfcnpre4.3 𝑇 = 𝐽
4 rfcnpre4.4 𝐴 = { 𝑡𝑇 ∣ ( 𝐹𝑡 ) ≤ 𝐵 }
5 rfcnpre4.5 ( 𝜑𝐵 ∈ ℝ )
6 rfcnpre4.6 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
7 eqid ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 )
8 2 3 7 6 fcnre ( 𝜑𝐹 : 𝑇 ⟶ ℝ )
9 ffn ( 𝐹 : 𝑇 ⟶ ℝ → 𝐹 Fn 𝑇 )
10 elpreima ( 𝐹 Fn 𝑇 → ( 𝑠 ∈ ( 𝐹 “ ( -∞ (,] 𝐵 ) ) ↔ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) ∈ ( -∞ (,] 𝐵 ) ) ) )
11 8 9 10 3syl ( 𝜑 → ( 𝑠 ∈ ( 𝐹 “ ( -∞ (,] 𝐵 ) ) ↔ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) ∈ ( -∞ (,] 𝐵 ) ) ) )
12 mnfxr -∞ ∈ ℝ*
13 5 rexrd ( 𝜑𝐵 ∈ ℝ* )
14 13 adantr ( ( 𝜑𝑠𝑇 ) → 𝐵 ∈ ℝ* )
15 elioc1 ( ( -∞ ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐹𝑠 ) ∈ ( -∞ (,] 𝐵 ) ↔ ( ( 𝐹𝑠 ) ∈ ℝ* ∧ -∞ < ( 𝐹𝑠 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) ) )
16 12 14 15 sylancr ( ( 𝜑𝑠𝑇 ) → ( ( 𝐹𝑠 ) ∈ ( -∞ (,] 𝐵 ) ↔ ( ( 𝐹𝑠 ) ∈ ℝ* ∧ -∞ < ( 𝐹𝑠 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) ) )
17 simpr3 ( ( ( 𝜑𝑠𝑇 ) ∧ ( ( 𝐹𝑠 ) ∈ ℝ* ∧ -∞ < ( 𝐹𝑠 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) ) → ( 𝐹𝑠 ) ≤ 𝐵 )
18 8 ffvelrnda ( ( 𝜑𝑠𝑇 ) → ( 𝐹𝑠 ) ∈ ℝ )
19 18 rexrd ( ( 𝜑𝑠𝑇 ) → ( 𝐹𝑠 ) ∈ ℝ* )
20 19 adantr ( ( ( 𝜑𝑠𝑇 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) → ( 𝐹𝑠 ) ∈ ℝ* )
21 18 adantr ( ( ( 𝜑𝑠𝑇 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) → ( 𝐹𝑠 ) ∈ ℝ )
22 mnflt ( ( 𝐹𝑠 ) ∈ ℝ → -∞ < ( 𝐹𝑠 ) )
23 21 22 syl ( ( ( 𝜑𝑠𝑇 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) → -∞ < ( 𝐹𝑠 ) )
24 simpr ( ( ( 𝜑𝑠𝑇 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) → ( 𝐹𝑠 ) ≤ 𝐵 )
25 20 23 24 3jca ( ( ( 𝜑𝑠𝑇 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) → ( ( 𝐹𝑠 ) ∈ ℝ* ∧ -∞ < ( 𝐹𝑠 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) )
26 17 25 impbida ( ( 𝜑𝑠𝑇 ) → ( ( ( 𝐹𝑠 ) ∈ ℝ* ∧ -∞ < ( 𝐹𝑠 ) ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) ↔ ( 𝐹𝑠 ) ≤ 𝐵 ) )
27 16 26 bitrd ( ( 𝜑𝑠𝑇 ) → ( ( 𝐹𝑠 ) ∈ ( -∞ (,] 𝐵 ) ↔ ( 𝐹𝑠 ) ≤ 𝐵 ) )
28 27 pm5.32da ( 𝜑 → ( ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) ∈ ( -∞ (,] 𝐵 ) ) ↔ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) ) )
29 11 28 bitrd ( 𝜑 → ( 𝑠 ∈ ( 𝐹 “ ( -∞ (,] 𝐵 ) ) ↔ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) ) )
30 nfcv 𝑡 𝑠
31 nfcv 𝑡 𝑇
32 1 30 nffv 𝑡 ( 𝐹𝑠 )
33 nfcv 𝑡
34 nfcv 𝑡 𝐵
35 32 33 34 nfbr 𝑡 ( 𝐹𝑠 ) ≤ 𝐵
36 fveq2 ( 𝑡 = 𝑠 → ( 𝐹𝑡 ) = ( 𝐹𝑠 ) )
37 36 breq1d ( 𝑡 = 𝑠 → ( ( 𝐹𝑡 ) ≤ 𝐵 ↔ ( 𝐹𝑠 ) ≤ 𝐵 ) )
38 30 31 35 37 elrabf ( 𝑠 ∈ { 𝑡𝑇 ∣ ( 𝐹𝑡 ) ≤ 𝐵 } ↔ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) ≤ 𝐵 ) )
39 29 38 bitr4di ( 𝜑 → ( 𝑠 ∈ ( 𝐹 “ ( -∞ (,] 𝐵 ) ) ↔ 𝑠 ∈ { 𝑡𝑇 ∣ ( 𝐹𝑡 ) ≤ 𝐵 } ) )
40 39 eqrdv ( 𝜑 → ( 𝐹 “ ( -∞ (,] 𝐵 ) ) = { 𝑡𝑇 ∣ ( 𝐹𝑡 ) ≤ 𝐵 } )
41 40 4 eqtr4di ( 𝜑 → ( 𝐹 “ ( -∞ (,] 𝐵 ) ) = 𝐴 )
42 iocmnfcld ( 𝐵 ∈ ℝ → ( -∞ (,] 𝐵 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
43 5 42 syl ( 𝜑 → ( -∞ (,] 𝐵 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
44 2 fveq2i ( Clsd ‘ 𝐾 ) = ( Clsd ‘ ( topGen ‘ ran (,) ) )
45 43 44 eleqtrrdi ( 𝜑 → ( -∞ (,] 𝐵 ) ∈ ( Clsd ‘ 𝐾 ) )
46 cnclima ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( -∞ (,] 𝐵 ) ∈ ( Clsd ‘ 𝐾 ) ) → ( 𝐹 “ ( -∞ (,] 𝐵 ) ) ∈ ( Clsd ‘ 𝐽 ) )
47 6 45 46 syl2anc ( 𝜑 → ( 𝐹 “ ( -∞ (,] 𝐵 ) ) ∈ ( Clsd ‘ 𝐽 ) )
48 41 47 eqeltrrd ( 𝜑𝐴 ∈ ( Clsd ‘ 𝐽 ) )