Metamath Proof Explorer


Theorem mbf0

Description: The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018)

Ref Expression
Assertion mbf0
|- (/) e. MblFn

Proof

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