Theorem rfcnpre2

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

	Ref	Expression
Hypotheses	rfcnpre2.1	|- F/_ x B
	rfcnpre2.2	|- F/_ x F
	rfcnpre2.3	|- F/ x ph
	rfcnpre2.4	|- K = ( topGen ` ran (,) )
	rfcnpre2.5	|- X = U. J
	rfcnpre2.6	|- A = { x e. X | ( F ` x ) < B }
	rfcnpre2.7	|- ( ph -> B e. RR* )
	rfcnpre2.8	|- ( ph -> F e. ( J Cn K ) )
Assertion	rfcnpre2	|- ( ph -> A e. J )

Proof

Step	Hyp	Ref	Expression
1		rfcnpre2.1	|- F/_ x B
2		rfcnpre2.2	|- F/_ x F
3		rfcnpre2.3	|- F/ x ph
4		rfcnpre2.4	|- K = ( topGen ` ran (,) )
5		rfcnpre2.5	|- X = U. J
6		rfcnpre2.6	|- A = { x e. X | ( F ` x ) < B }
7		rfcnpre2.7	|- ( ph -> B e. RR* )
8		rfcnpre2.8	|- ( ph -> F e. ( J Cn K ) )
9	2	nfcnv	|- F/_ x `' F
10		nfcv	|- F/_ x -oo
11		nfcv	|- F/_ x (,)
12	10 11 1	nfov	|- F/_ x ( -oo (,) B )
13	9 12	nfima	|- F/_ x ( `' F " ( -oo (,) B ) )
14		nfrab1	|- F/_ x { x e. X | ( F ` x ) < B }
15		eqid	|- ( J Cn K ) = ( J Cn K )
16	4 5 15 8	fcnre	|- ( ph -> F : X --> RR )
17	16	ffvelrnda	|- ( ( ph /\ x e. X ) -> ( F ` x ) e. RR )
18		elioomnf	|- ( B e. RR* -> ( ( F ` x ) e. ( -oo (,) B ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < B ) ) )
19	7 18	syl	|- ( ph -> ( ( F ` x ) e. ( -oo (,) B ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < B ) ) )
20	19	baibd	|- ( ( ph /\ ( F ` x ) e. RR ) -> ( ( F ` x ) e. ( -oo (,) B ) <-> ( F ` x ) < B ) )
21	17 20	syldan	|- ( ( ph /\ x e. X ) -> ( ( F ` x ) e. ( -oo (,) B ) <-> ( F ` x ) < B ) )
22	21	pm5.32da	|- ( ph -> ( ( x e. X /\ ( F ` x ) e. ( -oo (,) B ) ) <-> ( x e. X /\ ( F ` x ) < B ) ) )
23		ffn	|- ( F : X --> RR -> F Fn X )
24		elpreima	|- ( F Fn X -> ( x e. ( `' F " ( -oo (,) B ) ) <-> ( x e. X /\ ( F ` x ) e. ( -oo (,) B ) ) ) )
25	16 23 24	3syl	|- ( ph -> ( x e. ( `' F " ( -oo (,) B ) ) <-> ( x e. X /\ ( F ` x ) e. ( -oo (,) B ) ) ) )
26		rabid	|- ( x e. { x e. X | ( F ` x ) < B } <-> ( x e. X /\ ( F ` x ) < B ) )
27	26	a1i	|- ( ph -> ( x e. { x e. X | ( F ` x ) < B } <-> ( x e. X /\ ( F ` x ) < B ) ) )
28	22 25 27	3bitr4d	|- ( ph -> ( x e. ( `' F " ( -oo (,) B ) ) <-> x e. { x e. X | ( F ` x ) < B } ) )
29	3 13 14 28	eqrd	|- ( ph -> ( `' F " ( -oo (,) B ) ) = { x e. X | ( F ` x ) < B } )
30	29 6	eqtr4di	|- ( ph -> ( `' F " ( -oo (,) B ) ) = A )
31		iooretop	|- ( -oo (,) B ) e. ( topGen ` ran (,) )
32	31	a1i	|- ( ph -> ( -oo (,) B ) e. ( topGen ` ran (,) ) )
33	32 4	eleqtrrdi	|- ( ph -> ( -oo (,) B ) e. K )
34		cnima	|- ( ( F e. ( J Cn K ) /\ ( -oo (,) B ) e. K ) -> ( `' F " ( -oo (,) B ) ) e. J )
35	8 33 34	syl2anc	|- ( ph -> ( `' F " ( -oo (,) B ) ) e. J )
36	30 35	eqeltrrd	|- ( ph -> A e. J )