Metamath Proof Explorer

Theorem mbfid

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

Ref Expression
Assertion mbfid ⊢ A ∈ dom ⁡ vol → I ↾ A ∈ MblFn

Proof

Step Hyp Ref Expression
1 cnvresima ⊢ I ↾ A -1 x = I -1 x ∩ A
2 cnvi ⊢ I -1 = I
3 2 imaeq1i ⊢ I -1 x = I x
4 imai ⊢ I x = x
5 3 4 eqtri ⊢ I -1 x = x
6 5 ineq1i ⊢ I -1 x ∩ A = x ∩ A
7 1 6 eqtri ⊢ I ↾ A -1 x = x ∩ A
8 ioof ⊢ . : ℝ * × ℝ * ⟶ 𝒫 ℝ
9 ffn ⊢ . : ℝ * × ℝ * ⟶ 𝒫 ℝ → . Fn ℝ * × ℝ *
10 ovelrn ⊢ . Fn ℝ * × ℝ * → x ∈ ran ⁡ . ↔ ∃ y ∈ ℝ * ∃ z ∈ ℝ * x = y z
11 8 9 10 mp2b ⊢ x ∈ ran ⁡ . ↔ ∃ y ∈ ℝ * ∃ z ∈ ℝ * x = y z
12 id ⊢ x = y z → x = y z
13 ioombl ⊢ y z ∈ dom ⁡ vol
14 12 13 eqeltrdi ⊢ x = y z → x ∈ dom ⁡ vol
15 14 a1i ⊢ y ∈ ℝ * ∧ z ∈ ℝ * → x = y z → x ∈ dom ⁡ vol
16 15 rexlimivv ⊢ ∃ y ∈ ℝ * ∃ z ∈ ℝ * x = y z → x ∈ dom ⁡ vol
17 11 16 sylbi ⊢ x ∈ ran ⁡ . → x ∈ dom ⁡ vol
18 id ⊢ A ∈ dom ⁡ vol → A ∈ dom ⁡ vol
19 inmbl ⊢ x ∈ dom ⁡ vol ∧ A ∈ dom ⁡ vol → x ∩ A ∈ dom ⁡ vol
20 17 18 19 syl2anr ⊢ A ∈ dom ⁡ vol ∧ x ∈ ran ⁡ . → x ∩ A ∈ dom ⁡ vol
21 7 20 eqeltrid ⊢ A ∈ dom ⁡ vol ∧ x ∈ ran ⁡ . → I ↾ A -1 x ∈ dom ⁡ vol
22 21 ralrimiva ⊢ A ∈ dom ⁡ vol → ∀ x ∈ ran ⁡ . I ↾ A -1 x ∈ 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 ∈ dom ⁡ vol → A ⊆ ℝ
27 fss ⊢ I ↾ A : A ⟶ A ∧ A ⊆ ℝ → I ↾ A : A ⟶ ℝ
28 25 26 27 sylancr ⊢ A ∈ dom ⁡ vol → I ↾ A : A ⟶ ℝ
29 ismbf ⊢ I ↾ A : A ⟶ ℝ → I ↾ A ∈ MblFn ↔ ∀ x ∈ ran ⁡ . I ↾ A -1 x ∈ dom ⁡ vol
30 28 29 syl ⊢ A ∈ dom ⁡ vol → I ↾ A ∈ MblFn ↔ ∀ x ∈ ran ⁡ . I ↾ A -1 x ∈ dom ⁡ vol
31 22 30 mpbird ⊢ A ∈ dom ⁡ vol → I ↾ A ∈ MblFn