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 φJTop
cnfsmf.k K=topGenran.
cnfsmf.f φFJ𝑡domFCnK
cnfsmf.s S=SalGenJ
Assertion cnfsmf φFSMblFnS

Proof

Step Hyp Ref Expression
1 cnfsmf.1 φJTop
2 cnfsmf.k K=topGenran.
3 cnfsmf.f φFJ𝑡domFCnK
4 cnfsmf.s S=SalGenJ
5 nfv aφ
6 1 4 salgencld φSSAlg
7 eqid J𝑡domF=J𝑡domF
8 eqid K=K
9 7 8 cnf FJ𝑡domFCnKF:J𝑡domFK
10 3 9 syl φF:J𝑡domFK
11 10 fdmd φdomF=J𝑡domF
12 ovex J𝑡domFV
13 12 uniex J𝑡domFV
14 13 a1i φJ𝑡domFV
15 11 14 eqeltrd φdomFV
16 1 15 unirestss φJ𝑡domFJ
17 4 sssalgen JTopJS
18 1 17 syl φJS
19 18 unissd φJS
20 16 19 sstrd φJ𝑡domFS
21 11 20 eqsstrd φdomFS
22 uniretop =topGenran.
23 2 unieqi K=topGenran.
24 22 23 eqtr4i =K
25 24 a1i φ=K
26 25 feq3d φF:J𝑡domFF:J𝑡domFK
27 10 26 mpbird φF:J𝑡domF
28 27 ffdmd φF:domF
29 ssrest SSAlgJSJ𝑡domFS𝑡domF
30 6 18 29 syl2anc φJ𝑡domFS𝑡domF
31 30 adantr φaJ𝑡domFS𝑡domF
32 11 rabeqdv φxdomF|Fx<a=xJ𝑡domF|Fx<a
33 32 adantr φaxdomF|Fx<a=xJ𝑡domF|Fx<a
34 nfcv _xa
35 nfcv _xF
36 nfv xφa
37 eqid xJ𝑡domF|Fx<a=xJ𝑡domF|Fx<a
38 rexr aa*
39 38 adantl φaa*
40 3 adantr φaFJ𝑡domFCnK
41 34 35 36 2 7 37 39 40 rfcnpre2 φaxJ𝑡domF|Fx<aJ𝑡domF
42 33 41 eqeltrd φaxdomF|Fx<aJ𝑡domF
43 31 42 sseldd φaxdomF|Fx<aS𝑡domF
44 5 6 21 28 43 issmfd φFSMblFnS