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 | |
|
cnfsmf.k | |
||
cnfsmf.f | |
||
cnfsmf.s | |
||
Assertion | cnfsmf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnfsmf.1 | |
|
2 | cnfsmf.k | |
|
3 | cnfsmf.f | |
|
4 | cnfsmf.s | |
|
5 | nfv | |
|
6 | 1 4 | salgencld | |
7 | eqid | |
|
8 | eqid | |
|
9 | 7 8 | cnf | |
10 | 3 9 | syl | |
11 | 10 | fdmd | |
12 | ovex | |
|
13 | 12 | uniex | |
14 | 13 | a1i | |
15 | 11 14 | eqeltrd | |
16 | 1 15 | unirestss | |
17 | 4 | sssalgen | |
18 | 1 17 | syl | |
19 | 18 | unissd | |
20 | 16 19 | sstrd | |
21 | 11 20 | eqsstrd | |
22 | uniretop | |
|
23 | 2 | unieqi | |
24 | 22 23 | eqtr4i | |
25 | 24 | a1i | |
26 | 25 | feq3d | |
27 | 10 26 | mpbird | |
28 | 27 | ffdmd | |
29 | ssrest | |
|
30 | 6 18 29 | syl2anc | |
31 | 30 | adantr | |
32 | 11 | rabeqdv | |
33 | 32 | adantr | |
34 | nfcv | |
|
35 | nfcv | |
|
36 | nfv | |
|
37 | eqid | |
|
38 | rexr | |
|
39 | 38 | adantl | |
40 | 3 | adantr | |
41 | 34 35 36 2 7 37 39 40 | rfcnpre2 | |
42 | 33 41 | eqeltrd | |
43 | 31 42 | sseldd | |
44 | 5 6 21 28 43 | issmfd | |