Metamath Proof Explorer

Theorem rfcnpre1

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

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

Proof

Step Hyp Ref Expression
1 rfcnpre1.1 
 |-  F/_ x B
2 rfcnpre1.2 
 |-  F/_ x F
3 rfcnpre1.3 
 |-  F/ x ph
4 rfcnpre1.4 
 |-  K = ( topGen ` ran (,) )
5 rfcnpre1.5 
 |-  X = U. J
6 rfcnpre1.6 
 |-  A = { x e. X | B < ( F ` x ) }
7 rfcnpre1.7 
 |-  ( ph -> B e. RR* )
8 rfcnpre1.8 
 |-  ( ph -> F e. ( J Cn K ) )
9 2 nfcnv 
 |-  F/_ x `' F
10 nfcv 
 |-  F/_ x (,)
11 nfcv 
 |-  F/_ x +oo
12 1 10 11 nfov 
 |-  F/_ x ( B (,) +oo )
13 9 12 nfima 
 |-  F/_ x ( `' F " ( B (,) +oo ) )
14 nfrab1 
 |-  F/_ x { x e. X | B < ( F ` x ) }
15 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
16 8 15 syl 
 |-  ( ph -> J e. Top )
17 istopon 
 |-  ( J e. ( TopOn ` X ) <-> ( J e. Top /\ X = U. J ) )
18 16 5 17 sylanblrc 
 |-  ( ph -> J e. ( TopOn ` X ) )
19 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
20 4 19 eqeltri 
 |-  K e. ( TopOn ` RR )
21 iscn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` RR ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> RR /\ A. y e. K ( `' F " y ) e. J ) ) )
22 18 20 21 sylancl 
 |-  ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> RR /\ A. y e. K ( `' F " y ) e. J ) ) )
23 8 22 mpbid 
 |-  ( ph -> ( F : X --> RR /\ A. y e. K ( `' F " y ) e. J ) )
24 23 simpld 
 |-  ( ph -> F : X --> RR )
25 24 ffvelcdmda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. RR )
26 elioopnf 
 |-  ( B e. RR* -> ( ( F ` x ) e. ( B (,) +oo ) <-> ( ( F ` x ) e. RR /\ B < ( F ` x ) ) ) )
27 7 26 syl 
 |-  ( ph -> ( ( F ` x ) e. ( B (,) +oo ) <-> ( ( F ` x ) e. RR /\ B < ( F ` x ) ) ) )
28 27 baibd 
 |-  ( ( ph /\ ( F ` x ) e. RR ) -> ( ( F ` x ) e. ( B (,) +oo ) <-> B < ( F ` x ) ) )
29 25 28 syldan 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) e. ( B (,) +oo ) <-> B < ( F ` x ) ) )
30 29 pm5.32da 
 |-  ( ph -> ( ( x e. X /\ ( F ` x ) e. ( B (,) +oo ) ) <-> ( x e. X /\ B < ( F ` x ) ) ) )
31 ffn 
 |-  ( F : X --> RR -> F Fn X )
32 elpreima 
 |-  ( F Fn X -> ( x e. ( `' F " ( B (,) +oo ) ) <-> ( x e. X /\ ( F ` x ) e. ( B (,) +oo ) ) ) )
33 24 31 32 3syl 
 |-  ( ph -> ( x e. ( `' F " ( B (,) +oo ) ) <-> ( x e. X /\ ( F ` x ) e. ( B (,) +oo ) ) ) )
34 rabid 
 |-  ( x e. { x e. X | B < ( F ` x ) } <-> ( x e. X /\ B < ( F ` x ) ) )
35 34 a1i 
 |-  ( ph -> ( x e. { x e. X | B < ( F ` x ) } <-> ( x e. X /\ B < ( F ` x ) ) ) )
36 30 33 35 3bitr4d 
 |-  ( ph -> ( x e. ( `' F " ( B (,) +oo ) ) <-> x e. { x e. X | B < ( F ` x ) } ) )
37 3 13 14 36 eqrd 
 |-  ( ph -> ( `' F " ( B (,) +oo ) ) = { x e. X | B < ( F ` x ) } )
38 37 6 eqtr4di 
 |-  ( ph -> ( `' F " ( B (,) +oo ) ) = A )
39 iooretop 
 |-  ( B (,) +oo ) e. ( topGen ` ran (,) )
40 39 4 eleqtrri 
 |-  ( B (,) +oo ) e. K
41 cnima 
 |-  ( ( F e. ( J Cn K ) /\ ( B (,) +oo ) e. K ) -> ( `' F " ( B (,) +oo ) ) e. J )
42 8 40 41 sylancl 
 |-  ( ph -> ( `' F " ( B (,) +oo ) ) e. J )
43 38 42 eqeltrrd 
 |-  ( ph -> A e. J )