Metamath Proof Explorer

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 
|- F/_ t F
rfcnpre3.3 
|- K = ( topGen ` ran (,) )
rfcnpre3.4 
|- T = U. J
rfcnpre3.5 
|- A = { t e. T | B <_ ( F ` t ) }
rfcnpre3.6 
|- ( ph -> B e. RR )
rfcnpre3.8 
|- ( ph -> F e. ( J Cn K ) )
Assertion rfcnpre3 
|- ( ph -> A e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 rfcnpre3.2 
 |-  F/_ t F
2 rfcnpre3.3 
 |-  K = ( topGen ` ran (,) )
3 rfcnpre3.4 
 |-  T = U. J
4 rfcnpre3.5 
 |-  A = { t e. T | B <_ ( F ` t ) }
5 rfcnpre3.6 
 |-  ( ph -> B e. RR )
6 rfcnpre3.8 
 |-  ( ph -> F e. ( J Cn K ) )
7 eqid 
 |-  ( J Cn K ) = ( J Cn K )
8 2 3 7 6 fcnre 
 |-  ( ph -> F : T --> RR )
9 ffn 
 |-  ( F : T --> RR -> F Fn T )
10 elpreima 
 |-  ( F Fn T -> ( s e. ( `' F " ( B [,) +oo ) ) <-> ( s e. T /\ ( F ` s ) e. ( B [,) +oo ) ) ) )
11 8 9 10 3syl 
 |-  ( ph -> ( s e. ( `' F " ( B [,) +oo ) ) <-> ( s e. T /\ ( F ` s ) e. ( B [,) +oo ) ) ) )
12 5 rexrd 
 |-  ( ph -> B e. RR* )
13 12 adantr 
 |-  ( ( ph /\ s e. T ) -> B e. RR* )
14 pnfxr 
 |-  +oo e. RR*
15 elico1 
 |-  ( ( B e. RR* /\ +oo e. RR* ) -> ( ( F ` s ) e. ( B [,) +oo ) <-> ( ( F ` s ) e. RR* /\ B <_ ( F ` s ) /\ ( F ` s ) < +oo ) ) )
16 13 14 15 sylancl 
 |-  ( ( ph /\ s e. T ) -> ( ( F ` s ) e. ( B [,) +oo ) <-> ( ( F ` s ) e. RR* /\ B <_ ( F ` s ) /\ ( F ` s ) < +oo ) ) )
17 simpr2 
 |-  ( ( ( ph /\ s e. T ) /\ ( ( F ` s ) e. RR* /\ B <_ ( F ` s ) /\ ( F ` s ) < +oo ) ) -> B <_ ( F ` s ) )
18 8 ffvelrnda 
 |-  ( ( ph /\ s e. T ) -> ( F ` s ) e. RR )
19 18 rexrd 
 |-  ( ( ph /\ s e. T ) -> ( F ` s ) e. RR* )
20 19 adantr 
 |-  ( ( ( ph /\ s e. T ) /\ B <_ ( F ` s ) ) -> ( F ` s ) e. RR* )
21 simpr 
 |-  ( ( ( ph /\ s e. T ) /\ B <_ ( F ` s ) ) -> B <_ ( F ` s ) )
22 18 adantr 
 |-  ( ( ( ph /\ s e. T ) /\ B <_ ( F ` s ) ) -> ( F ` s ) e. RR )
23 ltpnf 
 |-  ( ( F ` s ) e. RR -> ( F ` s ) < +oo )
24 22 23 syl 
 |-  ( ( ( ph /\ s e. T ) /\ B <_ ( F ` s ) ) -> ( F ` s ) < +oo )
25 20 21 24 3jca 
 |-  ( ( ( ph /\ s e. T ) /\ B <_ ( F ` s ) ) -> ( ( F ` s ) e. RR* /\ B <_ ( F ` s ) /\ ( F ` s ) < +oo ) )
26 17 25 impbida 
 |-  ( ( ph /\ s e. T ) -> ( ( ( F ` s ) e. RR* /\ B <_ ( F ` s ) /\ ( F ` s ) < +oo ) <-> B <_ ( F ` s ) ) )
27 16 26 bitrd 
 |-  ( ( ph /\ s e. T ) -> ( ( F ` s ) e. ( B [,) +oo ) <-> B <_ ( F ` s ) ) )
28 27 pm5.32da 
 |-  ( ph -> ( ( s e. T /\ ( F ` s ) e. ( B [,) +oo ) ) <-> ( s e. T /\ B <_ ( F ` s ) ) ) )
29 11 28 bitrd 
 |-  ( ph -> ( s e. ( `' F " ( B [,) +oo ) ) <-> ( s e. T /\ B <_ ( F ` s ) ) ) )
30 nfcv 
 |-  F/_ t s
31 nfcv 
 |-  F/_ t T
32 nfcv 
 |-  F/_ t B
33 nfcv 
 |-  F/_ t <_
34 1 30 nffv 
 |-  F/_ t ( F ` s )
35 32 33 34 nfbr 
 |-  F/ t B <_ ( F ` s )
36 fveq2 
 |-  ( t = s -> ( F ` t ) = ( F ` s ) )
37 36 breq2d 
 |-  ( t = s -> ( B <_ ( F ` t ) <-> B <_ ( F ` s ) ) )
38 30 31 35 37 elrabf 
 |-  ( s e. { t e. T | B <_ ( F ` t ) } <-> ( s e. T /\ B <_ ( F ` s ) ) )
39 29 38 bitr4di 
 |-  ( ph -> ( s e. ( `' F " ( B [,) +oo ) ) <-> s e. { t e. T | B <_ ( F ` t ) } ) )
40 39 eqrdv 
 |-  ( ph -> ( `' F " ( B [,) +oo ) ) = { t e. T | B <_ ( F ` t ) } )
41 40 4 eqtr4di 
 |-  ( ph -> ( `' F " ( B [,) +oo ) ) = A )
42 icopnfcld 
 |-  ( B e. RR -> ( B [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
43 5 42 syl 
 |-  ( ph -> ( B [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
44 2 fveq2i 
 |-  ( Clsd ` K ) = ( Clsd ` ( topGen ` ran (,) ) )
45 43 44 eleqtrrdi 
 |-  ( ph -> ( B [,) +oo ) e. ( Clsd ` K ) )
46 cnclima 
 |-  ( ( F e. ( J Cn K ) /\ ( B [,) +oo ) e. ( Clsd ` K ) ) -> ( `' F " ( B [,) +oo ) ) e. ( Clsd ` J ) )
47 6 45 46 syl2anc 
 |-  ( ph -> ( `' F " ( B [,) +oo ) ) e. ( Clsd ` J ) )
48 41 47 eqeltrrd 
 |-  ( ph -> A e. ( Clsd ` J ) )