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 )

Metamath Proof Explorer

Theorem mbfid

Proof