Metamath Proof Explorer

Theorem cnfsmf

Description: A continuous function is measurable. Proposition 121D (b) of Fremlin1 p. 36 is a special case of this theorem, where the topology on the domain is induced by the standard topology on n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses cnfsmf.1 
|- ( ph -> J e. Top )
cnfsmf.k 
|- K = ( topGen ` ran (,) )
cnfsmf.f 
|- ( ph -> F e. ( ( J |`t dom F ) Cn K ) )
cnfsmf.s 
|- S = ( SalGen ` J )
Assertion cnfsmf 
|- ( ph -> F e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 cnfsmf.1 
 |-  ( ph -> J e. Top )
2 cnfsmf.k 
 |-  K = ( topGen ` ran (,) )
3 cnfsmf.f 
 |-  ( ph -> F e. ( ( J |`t dom F ) Cn K ) )
4 cnfsmf.s 
 |-  S = ( SalGen ` J )
5 nfv 
 |-  F/ a ph
6 1 4 salgencld 
 |-  ( ph -> S e. SAlg )
7 eqid 
 |-  U. ( J |`t dom F ) = U. ( J |`t dom F )
8 eqid 
 |-  U. K = U. K
9 7 8 cnf 
 |-  ( F e. ( ( J |`t dom F ) Cn K ) -> F : U. ( J |`t dom F ) --> U. K )
10 3 9 syl 
 |-  ( ph -> F : U. ( J |`t dom F ) --> U. K )
11 10 fdmd 
 |-  ( ph -> dom F = U. ( J |`t dom F ) )
12 ovex 
 |-  ( J |`t dom F ) e. _V
13 12 uniex 
 |-  U. ( J |`t dom F ) e. _V
14 13 a1i 
 |-  ( ph -> U. ( J |`t dom F ) e. _V )
15 11 14 eqeltrd 
 |-  ( ph -> dom F e. _V )
16 1 15 unirestss 
 |-  ( ph -> U. ( J |`t dom F ) C_ U. J )
17 4 sssalgen 
 |-  ( J e. Top -> J C_ S )
18 1 17 syl 
 |-  ( ph -> J C_ S )
19 18 unissd 
 |-  ( ph -> U. J C_ U. S )
20 16 19 sstrd 
 |-  ( ph -> U. ( J |`t dom F ) C_ U. S )
21 11 20 eqsstrd 
 |-  ( ph -> dom F C_ U. S )
22 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
23 2 unieqi 
 |-  U. K = U. ( topGen ` ran (,) )
24 22 23 eqtr4i 
 |-  RR = U. K
25 24 a1i 
 |-  ( ph -> RR = U. K )
26 25 feq3d 
 |-  ( ph -> ( F : U. ( J |`t dom F ) --> RR <-> F : U. ( J |`t dom F ) --> U. K ) )
27 10 26 mpbird 
 |-  ( ph -> F : U. ( J |`t dom F ) --> RR )
28 27 ffdmd 
 |-  ( ph -> F : dom F --> RR )
29 ssrest 
 |-  ( ( S e. SAlg /\ J C_ S ) -> ( J |`t dom F ) C_ ( S |`t dom F ) )
30 6 18 29 syl2anc 
 |-  ( ph -> ( J |`t dom F ) C_ ( S |`t dom F ) )
31 30 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( J |`t dom F ) C_ ( S |`t dom F ) )
32 11 rabeqdv 
 |-  ( ph -> { x e. dom F | ( F ` x ) < a } = { x e. U. ( J |`t dom F ) | ( F ` x ) < a } )
33 32 adantr 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } = { x e. U. ( J |`t dom F ) | ( F ` x ) < a } )
34 nfcv 
 |-  F/_ x a
35 nfcv 
 |-  F/_ x F
36 nfv 
 |-  F/ x ( ph /\ a e. RR )
37 eqid 
 |-  { x e. U. ( J |`t dom F ) | ( F ` x ) < a } = { x e. U. ( J |`t dom F ) | ( F ` x ) < a }
38 rexr 
 |-  ( a e. RR -> a e. RR* )
39 38 adantl 
 |-  ( ( ph /\ a e. RR ) -> a e. RR* )
40 3 adantr 
 |-  ( ( ph /\ a e. RR ) -> F e. ( ( J |`t dom F ) Cn K ) )
41 34 35 36 2 7 37 39 40 rfcnpre2 
 |-  ( ( ph /\ a e. RR ) -> { x e. U. ( J |`t dom F ) | ( F ` x ) < a } e. ( J |`t dom F ) )
42 33 41 eqeltrd 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } e. ( J |`t dom F ) )
43 31 42 sseldd 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) )
44 5 6 21 28 43 issmfd 
 |-  ( ph -> F e. ( SMblFn ` S ) )