mbfid

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

		Ref	Expression
	Assertion	mbfid	$⊢ A \in dom vol \to {I ↾}_{A} \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		cnvresima	$⊢ {({I ↾}_{A})}^{-1} [x] = I^{-1} [x] \cap 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] \cap A = x \cap A$
7	1 6	eqtri	$⊢ {({I ↾}_{A})}^{-1} [x] = x \cap A$
8		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
9		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
10		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (x \in ran (.) \leftrightarrow \exists y \in ℝ^{} \exists z \in ℝ^{} x = (y, z))$
11	8 9 10	mp2b	$⊢ x \in ran (.) \leftrightarrow \exists y \in ℝ^{} \exists z \in ℝ^{} x = (y, z)$
12		id	$⊢ x = (y, z) \to x = (y, z)$
13		ioombl	$⊢ (y, z) \in dom vol$
14	12 13	eqeltrdi	$⊢ x = (y, z) \to x \in dom vol$
15	14	a1i	$⊢ (y \in ℝ^{} \land z \in ℝ^{}) \to (x = (y, z) \to x \in dom vol)$
16	15	rexlimivv	$⊢ \exists y \in ℝ^{} \exists z \in ℝ^{} x = (y, z) \to x \in dom vol$
17	11 16	sylbi	$⊢ x \in ran (.) \to x \in dom vol$
18		id	$⊢ A \in dom vol \to A \in dom vol$
19		inmbl	$⊢ (x \in dom vol \land A \in dom vol) \to x \cap A \in dom vol$
20	17 18 19	syl2anr	$⊢ (A \in dom vol \land x \in ran (.)) \to x \cap A \in dom vol$
21	7 20	eqeltrid	$⊢ (A \in dom vol \land x \in ran (.)) \to {({I ↾}_{A})}^{-1} [x] \in dom vol$
22	21	ralrimiva	$⊢ A \in dom vol \to \forall x \in ran (.) {({I ↾}_{A})}^{-1} [x] \in dom vol$
23		f1oi	$⊢ ({I ↾}_{A}) : A \underset{1-1 onto}{⟶} A$
24		f1of	$⊢ ({I ↾}_{A}) : A \underset{1-1 onto}{⟶} A \to ({I ↾}_{A}) : A ⟶ A$
25	23 24	ax-mp	$⊢ ({I ↾}_{A}) : A ⟶ A$
26		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
27		fss	$⊢ (({I ↾}_{A}) : A ⟶ A \land A \subseteq ℝ) \to ({I ↾}_{A}) : A ⟶ ℝ$
28	25 26 27	sylancr	$⊢ A \in dom vol \to ({I ↾}_{A}) : A ⟶ ℝ$
29		ismbf	$⊢ ({I ↾}_{A}) : A ⟶ ℝ \to ({I ↾}_{A} \in MblFn \leftrightarrow \forall x \in ran (.) {({I ↾}_{A})}^{-1} [x] \in dom vol)$
30	28 29	syl	$⊢ A \in dom vol \to ({I ↾}_{A} \in MblFn \leftrightarrow \forall x \in ran (.) {({I ↾}_{A})}^{-1} [x] \in dom vol)$
31	22 30	mpbird	$⊢ A \in dom vol \to {I ↾}_{A} \in MblFn$

Metamath Proof Explorer

Theorem mbfid

Proof