Metamath Proof Explorer

Theorem rfcnpre4

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

Ref Expression
Hypotheses rfcnpre4.1 
|- F/_ t F
rfcnpre4.2 
|- K = ( topGen ` ran (,) )
rfcnpre4.3 
|- T = U. J
rfcnpre4.4 
|- A = { t e. T | ( F ` t ) <_ B }
rfcnpre4.5 
|- ( ph -> B e. RR )
rfcnpre4.6 
|- ( ph -> F e. ( J Cn K ) )
Assertion rfcnpre4 
|- ( ph -> A e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 rfcnpre4.1 
 |-  F/_ t F
2 rfcnpre4.2 
 |-  K = ( topGen ` ran (,) )
3 rfcnpre4.3 
 |-  T = U. J
4 rfcnpre4.4 
 |-  A = { t e. T | ( F ` t ) <_ B }
5 rfcnpre4.5 
 |-  ( ph -> B e. RR )
6 rfcnpre4.6 
 |-  ( 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 " ( -oo (,] B ) ) <-> ( s e. T /\ ( F ` s ) e. ( -oo (,] B ) ) ) )
11 8 9 10 3syl 
 |-  ( ph -> ( s e. ( `' F " ( -oo (,] B ) ) <-> ( s e. T /\ ( F ` s ) e. ( -oo (,] B ) ) ) )
12 mnfxr 
 |-  -oo e. RR*
13 5 rexrd 
 |-  ( ph -> B e. RR* )
14 13 adantr 
 |-  ( ( ph /\ s e. T ) -> B e. RR* )
15 elioc1 
 |-  ( ( -oo e. RR* /\ B e. RR* ) -> ( ( F ` s ) e. ( -oo (,] B ) <-> ( ( F ` s ) e. RR* /\ -oo < ( F ` s ) /\ ( F ` s ) <_ B ) ) )
16 12 14 15 sylancr 
 |-  ( ( ph /\ s e. T ) -> ( ( F ` s ) e. ( -oo (,] B ) <-> ( ( F ` s ) e. RR* /\ -oo < ( F ` s ) /\ ( F ` s ) <_ B ) ) )
17 simpr3 
 |-  ( ( ( ph /\ s e. T ) /\ ( ( F ` s ) e. RR* /\ -oo < ( F ` s ) /\ ( F ` s ) <_ B ) ) -> ( F ` s ) <_ B )
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 ) /\ ( F ` s ) <_ B ) -> ( F ` s ) e. RR* )
21 18 adantr 
 |-  ( ( ( ph /\ s e. T ) /\ ( F ` s ) <_ B ) -> ( F ` s ) e. RR )
22 mnflt 
 |-  ( ( F ` s ) e. RR -> -oo < ( F ` s ) )
23 21 22 syl 
 |-  ( ( ( ph /\ s e. T ) /\ ( F ` s ) <_ B ) -> -oo < ( F ` s ) )
24 simpr 
 |-  ( ( ( ph /\ s e. T ) /\ ( F ` s ) <_ B ) -> ( F ` s ) <_ B )
25 20 23 24 3jca 
 |-  ( ( ( ph /\ s e. T ) /\ ( F ` s ) <_ B ) -> ( ( F ` s ) e. RR* /\ -oo < ( F ` s ) /\ ( F ` s ) <_ B ) )
26 17 25 impbida 
 |-  ( ( ph /\ s e. T ) -> ( ( ( F ` s ) e. RR* /\ -oo < ( F ` s ) /\ ( F ` s ) <_ B ) <-> ( F ` s ) <_ B ) )
27 16 26 bitrd 
 |-  ( ( ph /\ s e. T ) -> ( ( F ` s ) e. ( -oo (,] B ) <-> ( F ` s ) <_ B ) )
28 27 pm5.32da 
 |-  ( ph -> ( ( s e. T /\ ( F ` s ) e. ( -oo (,] B ) ) <-> ( s e. T /\ ( F ` s ) <_ B ) ) )
29 11 28 bitrd 
 |-  ( ph -> ( s e. ( `' F " ( -oo (,] B ) ) <-> ( s e. T /\ ( F ` s ) <_ B ) ) )
30 nfcv 
 |-  F/_ t s
31 nfcv 
 |-  F/_ t T
32 1 30 nffv 
 |-  F/_ t ( F ` s )
33 nfcv 
 |-  F/_ t <_
34 nfcv 
 |-  F/_ t B
35 32 33 34 nfbr 
 |-  F/ t ( F ` s ) <_ B
36 fveq2 
 |-  ( t = s -> ( F ` t ) = ( F ` s ) )
37 36 breq1d 
 |-  ( t = s -> ( ( F ` t ) <_ B <-> ( F ` s ) <_ B ) )
38 30 31 35 37 elrabf 
 |-  ( s e. { t e. T | ( F ` t ) <_ B } <-> ( s e. T /\ ( F ` s ) <_ B ) )
39 29 38 bitr4di 
 |-  ( ph -> ( s e. ( `' F " ( -oo (,] B ) ) <-> s e. { t e. T | ( F ` t ) <_ B } ) )
40 39 eqrdv 
 |-  ( ph -> ( `' F " ( -oo (,] B ) ) = { t e. T | ( F ` t ) <_ B } )
41 40 4 eqtr4di 
 |-  ( ph -> ( `' F " ( -oo (,] B ) ) = A )
42 iocmnfcld 
 |-  ( B e. RR -> ( -oo (,] B ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
43 5 42 syl 
 |-  ( ph -> ( -oo (,] B ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
44 2 fveq2i 
 |-  ( Clsd ` K ) = ( Clsd ` ( topGen ` ran (,) ) )
45 43 44 eleqtrrdi 
 |-  ( ph -> ( -oo (,] B ) e. ( Clsd ` K ) )
46 cnclima 
 |-  ( ( F e. ( J Cn K ) /\ ( -oo (,] B ) e. ( Clsd ` K ) ) -> ( `' F " ( -oo (,] B ) ) e. ( Clsd ` J ) )
47 6 45 46 syl2anc 
 |-  ( ph -> ( `' F " ( -oo (,] B ) ) e. ( Clsd ` J ) )
48 41 47 eqeltrrd 
 |-  ( ph -> A e. ( Clsd ` J ) )