Metamath Proof Explorer

Theorem mbfid

Description: The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfid 
|- ( A e. dom vol -> ( _I |` A ) e. MblFn )

Proof

Step Hyp Ref Expression
1 cnvresima 
 |-  ( `' ( _I |` A ) " x ) = ( ( `' _I " x ) i^i A )
2 cnvi 
 |-  `' _I = _I
3 2 imaeq1i 
 |-  ( `' _I " x ) = ( _I " x )
4 imai 
 |-  ( _I " x ) = x
5 3 4 eqtri 
 |-  ( `' _I " x ) = x
6 5 ineq1i 
 |-  ( ( `' _I " x ) i^i A ) = ( x i^i A )
7 1 6 eqtri 
 |-  ( `' ( _I |` A ) " x ) = ( x i^i A )
8 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
9 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
10 ovelrn 
 |-  ( (,) Fn ( RR* X. RR* ) -> ( x e. ran (,) <-> E. y e. RR* E. z e. RR* x = ( y (,) z ) ) )
11 8 9 10 mp2b 
 |-  ( x e. ran (,) <-> E. y e. RR* E. z e. RR* x = ( y (,) z ) )
12 id 
 |-  ( x = ( y (,) z ) -> x = ( y (,) z ) )
13 ioombl 
 |-  ( y (,) z ) e. dom vol
14 12 13 eqeltrdi 
 |-  ( x = ( y (,) z ) -> x e. dom vol )
15 14 a1i 
 |-  ( ( y e. RR* /\ z e. RR* ) -> ( x = ( y (,) z ) -> x e. dom vol ) )
16 15 rexlimivv 
 |-  ( E. y e. RR* E. z e. RR* x = ( y (,) z ) -> x e. dom vol )
17 11 16 sylbi 
 |-  ( x e. ran (,) -> x e. dom vol )
18 id 
 |-  ( A e. dom vol -> A e. dom vol )
19 inmbl 
 |-  ( ( x e. dom vol /\ A e. dom vol ) -> ( x i^i A ) e. dom vol )
20 17 18 19 syl2anr 
 |-  ( ( A e. dom vol /\ x e. ran (,) ) -> ( x i^i A ) e. dom vol )
21 7 20 eqeltrid 
 |-  ( ( A e. dom vol /\ x e. ran (,) ) -> ( `' ( _I |` A ) " x ) e. dom vol )
22 21 ralrimiva 
 |-  ( A e. dom vol -> A. x e. ran (,) ( `' ( _I |` A ) " x ) e. dom vol )
23 f1oi 
 |-  ( _I |` A ) : A -1-1-onto-> A
24 f1of 
 |-  ( ( _I |` A ) : A -1-1-onto-> A -> ( _I |` A ) : A --> A )
25 23 24 ax-mp 
 |-  ( _I |` A ) : A --> A
26 mblss 
 |-  ( A e. dom vol -> A C_ RR )
27 fss 
 |-  ( ( ( _I |` A ) : A --> A /\ A C_ RR ) -> ( _I |` A ) : A --> RR )
28 25 26 27 sylancr 
 |-  ( A e. dom vol -> ( _I |` A ) : A --> RR )
29 ismbf 
 |-  ( ( _I |` A ) : A --> RR -> ( ( _I |` A ) e. MblFn <-> A. x e. ran (,) ( `' ( _I |` A ) " x ) e. dom vol ) )
30 28 29 syl 
 |-  ( A e. dom vol -> ( ( _I |` A ) e. MblFn <-> A. x e. ran (,) ( `' ( _I |` A ) " x ) e. dom vol ) )
31 22 30 mpbird 
 |-  ( A e. dom vol -> ( _I |` A ) e. MblFn )