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	ffvelcdmda	\|- ( ( 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 )

Metamath Proof Explorer

Theorem rfcnpre2

Proof