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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ )
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 ‘ 𝐽 ) )