# 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 ${⊢}{\phi }\to {J}\in \mathrm{Top}$
cnfsmf.k ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
cnfsmf.f ${⊢}{\phi }\to {F}\in \left(\left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)\mathrm{Cn}{K}\right)$
cnfsmf.s ${⊢}{S}=\mathrm{SalGen}\left({J}\right)$
Assertion cnfsmf ${⊢}{\phi }\to {F}\in \mathrm{SMblFn}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 cnfsmf.1 ${⊢}{\phi }\to {J}\in \mathrm{Top}$
2 cnfsmf.k ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
3 cnfsmf.f ${⊢}{\phi }\to {F}\in \left(\left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)\mathrm{Cn}{K}\right)$
4 cnfsmf.s ${⊢}{S}=\mathrm{SalGen}\left({J}\right)$
5 nfv ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}{\phi }$
6 1 4 salgencld ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
7 eqid ${⊢}\bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)=\bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)$
8 eqid ${⊢}\bigcup {K}=\bigcup {K}$
9 7 8 cnf ${⊢}{F}\in \left(\left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)\mathrm{Cn}{K}\right)\to {F}:\bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)⟶\bigcup {K}$
10 3 9 syl ${⊢}{\phi }\to {F}:\bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)⟶\bigcup {K}$
11 10 fdmd ${⊢}{\phi }\to \mathrm{dom}{F}=\bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)$
12 ovex ${⊢}{J}{↾}_{𝑡}\mathrm{dom}{F}\in \mathrm{V}$
13 12 uniex ${⊢}\bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)\in \mathrm{V}$
14 13 a1i ${⊢}{\phi }\to \bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)\in \mathrm{V}$
15 11 14 eqeltrd ${⊢}{\phi }\to \mathrm{dom}{F}\in \mathrm{V}$
16 1 15 unirestss ${⊢}{\phi }\to \bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)\subseteq \bigcup {J}$
17 4 sssalgen ${⊢}{J}\in \mathrm{Top}\to {J}\subseteq {S}$
18 1 17 syl ${⊢}{\phi }\to {J}\subseteq {S}$
19 18 unissd ${⊢}{\phi }\to \bigcup {J}\subseteq \bigcup {S}$
20 16 19 sstrd ${⊢}{\phi }\to \bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)\subseteq \bigcup {S}$
21 11 20 eqsstrd ${⊢}{\phi }\to \mathrm{dom}{F}\subseteq \bigcup {S}$
22 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
23 2 unieqi ${⊢}\bigcup {K}=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
24 22 23 eqtr4i ${⊢}ℝ=\bigcup {K}$
25 24 a1i ${⊢}{\phi }\to ℝ=\bigcup {K}$
26 25 feq3d ${⊢}{\phi }\to \left({F}:\bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)⟶ℝ↔{F}:\bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)⟶\bigcup {K}\right)$
27 10 26 mpbird ${⊢}{\phi }\to {F}:\bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)⟶ℝ$
28 27 ffdmd ${⊢}{\phi }\to {F}:\mathrm{dom}{F}⟶ℝ$
29 ssrest ${⊢}\left({S}\in \mathrm{SAlg}\wedge {J}\subseteq {S}\right)\to {J}{↾}_{𝑡}\mathrm{dom}{F}\subseteq {S}{↾}_{𝑡}\mathrm{dom}{F}$
30 6 18 29 syl2anc ${⊢}{\phi }\to {J}{↾}_{𝑡}\mathrm{dom}{F}\subseteq {S}{↾}_{𝑡}\mathrm{dom}{F}$
31 30 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {J}{↾}_{𝑡}\mathrm{dom}{F}\subseteq {S}{↾}_{𝑡}\mathrm{dom}{F}$
32 11 rabeqdv ${⊢}{\phi }\to \left\{{x}\in \mathrm{dom}{F}|{F}\left({x}\right)<{a}\right\}=\left\{{x}\in \bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)|{F}\left({x}\right)<{a}\right\}$
33 32 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{x}\in \mathrm{dom}{F}|{F}\left({x}\right)<{a}\right\}=\left\{{x}\in \bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)|{F}\left({x}\right)<{a}\right\}$
34 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{a}$
35 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
36 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {a}\in ℝ\right)$
37 eqid ${⊢}\left\{{x}\in \bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)|{F}\left({x}\right)<{a}\right\}=\left\{{x}\in \bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)|{F}\left({x}\right)<{a}\right\}$
38 rexr ${⊢}{a}\in ℝ\to {a}\in {ℝ}^{*}$
39 38 adantl ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {a}\in {ℝ}^{*}$
40 3 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {F}\in \left(\left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)\mathrm{Cn}{K}\right)$
41 34 35 36 2 7 37 39 40 rfcnpre2 ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{x}\in \bigcup \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)|{F}\left({x}\right)<{a}\right\}\in \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)$
42 33 41 eqeltrd ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{x}\in \mathrm{dom}{F}|{F}\left({x}\right)<{a}\right\}\in \left({J}{↾}_{𝑡}\mathrm{dom}{F}\right)$
43 31 42 sseldd ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{x}\in \mathrm{dom}{F}|{F}\left({x}\right)<{a}\right\}\in \left({S}{↾}_{𝑡}\mathrm{dom}{F}\right)$
44 5 6 21 28 43 issmfd ${⊢}{\phi }\to {F}\in \mathrm{SMblFn}\left({S}\right)$