Description: The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | mbf0 | |- (/) e. MblFn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0xp | |- ( (/) X. { 1 } ) = (/) |
|
2 | 0mbl | |- (/) e. dom vol |
|
3 | ax-1cn | |- 1 e. CC |
|
4 | mbfconst | |- ( ( (/) e. dom vol /\ 1 e. CC ) -> ( (/) X. { 1 } ) e. MblFn ) |
|
5 | 2 3 4 | mp2an | |- ( (/) X. { 1 } ) e. MblFn |
6 | 1 5 | eqeltrri | |- (/) e. MblFn |