Metamath Proof Explorer

Theorem mbfeqa

Description: If two functions are equal almost everywhere, then one is measurable iff the other is. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by Mario Carneiro, 2-Sep-2014)

		Ref	Expression
	Hypotheses	mbfeqa.1	$⊢ φ \to A \subseteq ℝ$
		mbfeqa.2	$⊢ φ \to {vol}^{*} (A) = 0$
		mbfeqa.3	$⊢ (φ \land x \in (B ∖ A)) \to C = D$
		mbfeqa.4	$⊢ (φ \land x \in B) \to C \in ℂ$
		mbfeqa.5	$⊢ (φ \land x \in B) \to D \in ℂ$
	Assertion	mbfeqa	$⊢ φ \to ((x \in B ⟼ C) \in MblFn \leftrightarrow (x \in B ⟼ D) \in MblFn)$

Proof

Step	Hyp	Ref	Expression
1		mbfeqa.1	$⊢ φ \to A \subseteq ℝ$
2		mbfeqa.2	$⊢ φ \to {vol}^{*} (A) = 0$
3		mbfeqa.3	$⊢ (φ \land x \in (B ∖ A)) \to C = D$
4		mbfeqa.4	$⊢ (φ \land x \in B) \to C \in ℂ$
5		mbfeqa.5	$⊢ (φ \land x \in B) \to D \in ℂ$
6	3	fveq2d	$⊢ (φ \land x \in (B ∖ A)) \to ℜ (C) = ℜ (D)$
7	4	recld	$⊢ (φ \land x \in B) \to ℜ (C) \in ℝ$
8	5	recld	$⊢ (φ \land x \in B) \to ℜ (D) \in ℝ$
9	1 2 6 7 8	mbfeqalem2	$⊢ φ \to ((x \in B ⟼ ℜ (C)) \in MblFn \leftrightarrow (x \in B ⟼ ℜ (D)) \in MblFn)$
10	3	fveq2d	$⊢ (φ \land x \in (B ∖ A)) \to ℑ (C) = ℑ (D)$
11	4	imcld	$⊢ (φ \land x \in B) \to ℑ (C) \in ℝ$
12	5	imcld	$⊢ (φ \land x \in B) \to ℑ (D) \in ℝ$
13	1 2 10 11 12	mbfeqalem2	$⊢ φ \to ((x \in B ⟼ ℑ (C)) \in MblFn \leftrightarrow (x \in B ⟼ ℑ (D)) \in MblFn)$
14	9 13	anbi12d	$⊢ φ \to (((x \in B ⟼ ℜ (C)) \in MblFn \land (x \in B ⟼ ℑ (C)) \in MblFn) \leftrightarrow ((x \in B ⟼ ℜ (D)) \in MblFn \land (x \in B ⟼ ℑ (D)) \in MblFn))$
15	4	ismbfcn2	$⊢ φ \to ((x \in B ⟼ C) \in MblFn \leftrightarrow ((x \in B ⟼ ℜ (C)) \in MblFn \land (x \in B ⟼ ℑ (C)) \in MblFn))$
16	5	ismbfcn2	$⊢ φ \to ((x \in B ⟼ D) \in MblFn \leftrightarrow ((x \in B ⟼ ℜ (D)) \in MblFn \land (x \in B ⟼ ℑ (D)) \in MblFn))$
17	14 15 16	3bitr4d	$⊢ φ \to ((x \in B ⟼ C) \in MblFn \leftrightarrow (x \in B ⟼ D) \in MblFn)$