Theorem rfcnpre3

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

	Ref	Expression
Hypotheses	rfcnpre3.2	⊢ Ⅎ 𝑡 𝐹
	rfcnpre3.3	⊢ 𝐾 = ( topGen ‘ ran (,) )
	rfcnpre3.4	⊢ 𝑇 = ∪ 𝐽
	rfcnpre3.5	⊢ 𝐴 = { 𝑡 ∈ 𝑇 ∣ 𝐵 ≤ ( 𝐹 ‘ 𝑡 ) }
	rfcnpre3.6	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	rfcnpre3.8	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	rfcnpre3	⊢ ( 𝜑 → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		rfcnpre3.2	⊢ Ⅎ 𝑡 𝐹
2		rfcnpre3.3	⊢ 𝐾 = ( topGen ‘ ran (,) )
3		rfcnpre3.4	⊢ 𝑇 = ∪ 𝐽
4		rfcnpre3.5	⊢ 𝐴 = { 𝑡 ∈ 𝑇 ∣ 𝐵 ≤ ( 𝐹 ‘ 𝑡 ) }
5		rfcnpre3.6	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
6		rfcnpre3.8	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
7		eqid	⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 )
8	2 3 7 6	fcnre	⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
9		ffn	⊢ ( 𝐹 : 𝑇 ⟶ ℝ → 𝐹 Fn 𝑇 )
10		elpreima	⊢ ( 𝐹 Fn 𝑇 → ( 𝑠 ∈ ( ◡ 𝐹 “ ( 𝐵 [,) +∞ ) ) ↔ ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐵 [,) +∞ ) ) ) )
11	8 9 10	3syl	⊢ ( 𝜑 → ( 𝑠 ∈ ( ◡ 𝐹 “ ( 𝐵 [,) +∞ ) ) ↔ ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐵 [,) +∞ ) ) ) )
12	5	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → 𝐵 ∈ ℝ* )
14		pnfxr	⊢ +∞ ∈ ℝ*
15		elico1	⊢ ( ( 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐵 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ* ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ∧ ( 𝐹 ‘ 𝑠 ) < +∞ ) ) )
16	13 14 15	sylancl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐵 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ* ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ∧ ( 𝐹 ‘ 𝑠 ) < +∞ ) ) )
17		simpr2	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ* ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ∧ ( 𝐹 ‘ 𝑠 ) < +∞ ) ) → 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) )
18	8	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ )
19	18	rexrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ* )
20	19	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ* )
21		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) → 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) )
22	18	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ )
23		ltpnf	⊢ ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ → ( 𝐹 ‘ 𝑠 ) < +∞ )
24	22 23	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) → ( 𝐹 ‘ 𝑠 ) < +∞ )
25	20 21 24	3jca	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) → ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ* ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ∧ ( 𝐹 ‘ 𝑠 ) < +∞ ) )
26	17 25	impbida	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ* ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ∧ ( 𝐹 ‘ 𝑠 ) < +∞ ) ↔ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) )
27	16 26	bitrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐵 [,) +∞ ) ↔ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) )
28	27	pm5.32da	⊢ ( 𝜑 → ( ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐵 [,) +∞ ) ) ↔ ( 𝑠 ∈ 𝑇 ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) ) )
29	11 28	bitrd	⊢ ( 𝜑 → ( 𝑠 ∈ ( ◡ 𝐹 “ ( 𝐵 [,) +∞ ) ) ↔ ( 𝑠 ∈ 𝑇 ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) ) )
30		nfcv	⊢ Ⅎ 𝑡 𝑠
31		nfcv	⊢ Ⅎ 𝑡 𝑇
32		nfcv	⊢ Ⅎ 𝑡 𝐵
33		nfcv	⊢ Ⅎ 𝑡 ≤
34	1 30	nffv	⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑠 )
35	32 33 34	nfbr	⊢ Ⅎ 𝑡 𝐵 ≤ ( 𝐹 ‘ 𝑠 )
36		fveq2	⊢ ( 𝑡 = 𝑠 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑠 ) )
37	36	breq2d	⊢ ( 𝑡 = 𝑠 → ( 𝐵 ≤ ( 𝐹 ‘ 𝑡 ) ↔ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) )
38	30 31 35 37	elrabf	⊢ ( 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 𝐵 ≤ ( 𝐹 ‘ 𝑡 ) } ↔ ( 𝑠 ∈ 𝑇 ∧ 𝐵 ≤ ( 𝐹 ‘ 𝑠 ) ) )
39	29 38	bitr4di	⊢ ( 𝜑 → ( 𝑠 ∈ ( ◡ 𝐹 “ ( 𝐵 [,) +∞ ) ) ↔ 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 𝐵 ≤ ( 𝐹 ‘ 𝑡 ) } ) )
40	39	eqrdv	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐵 [,) +∞ ) ) = { 𝑡 ∈ 𝑇 ∣ 𝐵 ≤ ( 𝐹 ‘ 𝑡 ) } )
41	40 4	eqtr4di	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐵 [,) +∞ ) ) = 𝐴 )
42		icopnfcld	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 [,) +∞ ) ∈ ( 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 ‘ 𝐽 ) )