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	$$⊢\underset{\_}{Ⅎ}tF$$
	rfcnpre3.3	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	rfcnpre3.4	$$⊢T=\bigcup J$$
	rfcnpre3.5	$$⊢A=\left\{t\in T|B\le F\left(t\right)\right\}$$
	rfcnpre3.6	$$⊢\phi \to B\in ℝ$$
	rfcnpre3.8	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
Assertion	rfcnpre3	$$⊢\phi \to A\in \mathrm{Clsd}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		rfcnpre3.2	$$⊢\underset{\_}{Ⅎ}tF$$
2		rfcnpre3.3	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3		rfcnpre3.4	$$⊢T=\bigcup J$$
4		rfcnpre3.5	$$⊢A=\left\{t\in T|B\le F\left(t\right)\right\}$$
5		rfcnpre3.6	$$⊢\phi \to B\in ℝ$$
6		rfcnpre3.8	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
7		eqid	$$⊢J\mathrm{Cn}K=J\mathrm{Cn}K$$
8	2 3 7 6	fcnre	$$⊢\phi \to F:T⟶ℝ$$
9		ffn	$$⊢F:T⟶ℝ\to FFnT$$
10		elpreima	$$⊢FFnT\to \left(s\in F^{-1}\left[\left[B,\mathrm{+\infty }\right)\right]\leftrightarrow \left(s\in T\wedge F\left(s\right)\in \left[B,\mathrm{+\infty }\right)\right)\right)$$
11	8 9 10	3syl	$$⊢\phi \to \left(s\in F^{-1}\left[\left[B,\mathrm{+\infty }\right)\right]\leftrightarrow \left(s\in T\wedge F\left(s\right)\in \left[B,\mathrm{+\infty }\right)\right)\right)$$
12	5	rexrd	$$⊢\phi \to B\in {ℝ}^{*}$$
13	12	adantr	$$⊢\left(\phi \wedge s\in T\right)\to B\in {ℝ}^{*}$$
14		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
15		elico1	$$⊢\left(B\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(F\left(s\right)\in \left[B,\mathrm{+\infty }\right)\leftrightarrow \left(F\left(s\right)\in {ℝ}^{*}\wedge B\le F\left(s\right)\wedge F\left(s\right)<\mathrm{+\infty }\right)\right)$$
16	13 14 15	sylancl	$$⊢\left(\phi \wedge s\in T\right)\to \left(F\left(s\right)\in \left[B,\mathrm{+\infty }\right)\leftrightarrow \left(F\left(s\right)\in {ℝ}^{*}\wedge B\le F\left(s\right)\wedge F\left(s\right)<\mathrm{+\infty }\right)\right)$$
17		simpr2	$$⊢\left(\left(\phi \wedge s\in T\right)\wedge \left(F\left(s\right)\in {ℝ}^{*}\wedge B\le F\left(s\right)\wedge F\left(s\right)<\mathrm{+\infty }\right)\right)\to B\le F\left(s\right)$$
18	8	ffvelrnda	$$⊢\left(\phi \wedge s\in T\right)\to F\left(s\right)\in ℝ$$
19	18	rexrd	$$⊢\left(\phi \wedge s\in T\right)\to F\left(s\right)\in {ℝ}^{*}$$
20	19	adantr	$$⊢\left(\left(\phi \wedge s\in T\right)\wedge B\le F\left(s\right)\right)\to F\left(s\right)\in {ℝ}^{*}$$
21		simpr	$$⊢\left(\left(\phi \wedge s\in T\right)\wedge B\le F\left(s\right)\right)\to B\le F\left(s\right)$$
22	18	adantr	$$⊢\left(\left(\phi \wedge s\in T\right)\wedge B\le F\left(s\right)\right)\to F\left(s\right)\in ℝ$$
23		ltpnf	$$⊢F\left(s\right)\in ℝ\to F\left(s\right)<\mathrm{+\infty }$$
24	22 23	syl	$$⊢\left(\left(\phi \wedge s\in T\right)\wedge B\le F\left(s\right)\right)\to F\left(s\right)<\mathrm{+\infty }$$
25	20 21 24	3jca	$$⊢\left(\left(\phi \wedge s\in T\right)\wedge B\le F\left(s\right)\right)\to \left(F\left(s\right)\in {ℝ}^{*}\wedge B\le F\left(s\right)\wedge F\left(s\right)<\mathrm{+\infty }\right)$$
26	17 25	impbida	$$⊢\left(\phi \wedge s\in T\right)\to \left(\left(F\left(s\right)\in {ℝ}^{*}\wedge B\le F\left(s\right)\wedge F\left(s\right)<\mathrm{+\infty }\right)\leftrightarrow B\le F\left(s\right)\right)$$
27	16 26	bitrd	$$⊢\left(\phi \wedge s\in T\right)\to \left(F\left(s\right)\in \left[B,\mathrm{+\infty }\right)\leftrightarrow B\le F\left(s\right)\right)$$
28	27	pm5.32da	$$⊢\phi \to \left(\left(s\in T\wedge F\left(s\right)\in \left[B,\mathrm{+\infty }\right)\right)\leftrightarrow \left(s\in T\wedge B\le F\left(s\right)\right)\right)$$
29	11 28	bitrd	$$⊢\phi \to \left(s\in F^{-1}\left[\left[B,\mathrm{+\infty }\right)\right]\leftrightarrow \left(s\in T\wedge B\le F\left(s\right)\right)\right)$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}ts$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}tT$$
32		nfcv	$$⊢\underset{\_}{Ⅎ}tB$$
33		nfcv	$$⊢\underset{\_}{Ⅎ}t\le$$
34	1 30	nffv	$$⊢\underset{\_}{Ⅎ}tF\left(s\right)$$
35	32 33 34	nfbr	$$⊢ℲtB\le F\left(s\right)$$
36		fveq2	$$⊢t=s\to F\left(t\right)=F\left(s\right)$$
37	36	breq2d	$$⊢t=s\to \left(B\le F\left(t\right)\leftrightarrow B\le F\left(s\right)\right)$$
38	30 31 35 37	elrabf	$$⊢s\in \left\{t\in T|B\le F\left(t\right)\right\}\leftrightarrow \left(s\in T\wedge B\le F\left(s\right)\right)$$
39	29 38	bitr4di	$$⊢\phi \to \left(s\in F^{-1}\left[\left[B,\mathrm{+\infty }\right)\right]\leftrightarrow s\in \left\{t\in T|B\le F\left(t\right)\right\}\right)$$
40	39	eqrdv	$$⊢\phi \to F^{-1}\left[\left[B,\mathrm{+\infty }\right)\right]=\left\{t\in T|B\le F\left(t\right)\right\}$$
41	40 4	eqtr4di	$$⊢\phi \to F^{-1}\left[\left[B,\mathrm{+\infty }\right)\right]=A$$
42		icopnfcld	$$⊢B\in ℝ\to \left[B,\mathrm{+\infty }\right)\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
43	5 42	syl	$$⊢\phi \to \left[B,\mathrm{+\infty }\right)\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
44	2	fveq2i	$$⊢\mathrm{Clsd}\left(K\right)=\mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
45	43 44	eleqtrrdi	$$⊢\phi \to \left[B,\mathrm{+\infty }\right)\in \mathrm{Clsd}\left(K\right)$$
46		cnclima	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge \left[B,\mathrm{+\infty }\right)\in \mathrm{Clsd}\left(K\right)\right)\to F^{-1}\left[\left[B,\mathrm{+\infty }\right)\right]\in \mathrm{Clsd}\left(J\right)$$
47	6 45 46	syl2anc	$$⊢\phi \to F^{-1}\left[\left[B,\mathrm{+\infty }\right)\right]\in \mathrm{Clsd}\left(J\right)$$
48	41 47	eqeltrrd	$$⊢\phi \to A\in \mathrm{Clsd}\left(J\right)$$