Metamath Proof Explorer


Theorem mbfid

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

Ref Expression
Assertion mbfid ( 𝐴 ∈ dom vol → ( I ↾ 𝐴 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 cnvresima ( ( I ↾ 𝐴 ) “ 𝑥 ) = ( ( I “ 𝑥 ) ∩ 𝐴 )
2 cnvi I = I
3 2 imaeq1i ( I “ 𝑥 ) = ( I “ 𝑥 )
4 imai ( I “ 𝑥 ) = 𝑥
5 3 4 eqtri ( I “ 𝑥 ) = 𝑥
6 5 ineq1i ( ( I “ 𝑥 ) ∩ 𝐴 ) = ( 𝑥𝐴 )
7 1 6 eqtri ( ( I ↾ 𝐴 ) “ 𝑥 ) = ( 𝑥𝐴 )
8 ioof (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
9 ffn ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
10 ovelrn ( (,) Fn ( ℝ* × ℝ* ) → ( 𝑥 ∈ ran (,) ↔ ∃ 𝑦 ∈ ℝ*𝑧 ∈ ℝ* 𝑥 = ( 𝑦 (,) 𝑧 ) ) )
11 8 9 10 mp2b ( 𝑥 ∈ ran (,) ↔ ∃ 𝑦 ∈ ℝ*𝑧 ∈ ℝ* 𝑥 = ( 𝑦 (,) 𝑧 ) )
12 id ( 𝑥 = ( 𝑦 (,) 𝑧 ) → 𝑥 = ( 𝑦 (,) 𝑧 ) )
13 ioombl ( 𝑦 (,) 𝑧 ) ∈ dom vol
14 12 13 eqeltrdi ( 𝑥 = ( 𝑦 (,) 𝑧 ) → 𝑥 ∈ dom vol )
15 14 a1i ( ( 𝑦 ∈ ℝ*𝑧 ∈ ℝ* ) → ( 𝑥 = ( 𝑦 (,) 𝑧 ) → 𝑥 ∈ dom vol ) )
16 15 rexlimivv ( ∃ 𝑦 ∈ ℝ*𝑧 ∈ ℝ* 𝑥 = ( 𝑦 (,) 𝑧 ) → 𝑥 ∈ dom vol )
17 11 16 sylbi ( 𝑥 ∈ ran (,) → 𝑥 ∈ dom vol )
18 id ( 𝐴 ∈ dom vol → 𝐴 ∈ dom vol )
19 inmbl ( ( 𝑥 ∈ dom vol ∧ 𝐴 ∈ dom vol ) → ( 𝑥𝐴 ) ∈ dom vol )
20 17 18 19 syl2anr ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ ran (,) ) → ( 𝑥𝐴 ) ∈ dom vol )
21 7 20 eqeltrid ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ ran (,) ) → ( ( I ↾ 𝐴 ) “ 𝑥 ) ∈ dom vol )
22 21 ralrimiva ( 𝐴 ∈ dom vol → ∀ 𝑥 ∈ ran (,) ( ( I ↾ 𝐴 ) “ 𝑥 ) ∈ dom vol )
23 f1oi ( I ↾ 𝐴 ) : 𝐴1-1-onto𝐴
24 f1of ( ( I ↾ 𝐴 ) : 𝐴1-1-onto𝐴 → ( I ↾ 𝐴 ) : 𝐴𝐴 )
25 23 24 ax-mp ( I ↾ 𝐴 ) : 𝐴𝐴
26 mblss ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
27 fss ( ( ( I ↾ 𝐴 ) : 𝐴𝐴𝐴 ⊆ ℝ ) → ( I ↾ 𝐴 ) : 𝐴 ⟶ ℝ )
28 25 26 27 sylancr ( 𝐴 ∈ dom vol → ( I ↾ 𝐴 ) : 𝐴 ⟶ ℝ )
29 ismbf ( ( I ↾ 𝐴 ) : 𝐴 ⟶ ℝ → ( ( I ↾ 𝐴 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ( I ↾ 𝐴 ) “ 𝑥 ) ∈ dom vol ) )
30 28 29 syl ( 𝐴 ∈ dom vol → ( ( I ↾ 𝐴 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ( I ↾ 𝐴 ) “ 𝑥 ) ∈ dom vol ) )
31 22 30 mpbird ( 𝐴 ∈ dom vol → ( I ↾ 𝐴 ) ∈ MblFn )