Theorem ismbf2d

Description: Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Hypotheses	ismbf2d.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
	ismbf2d.2	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
	ismbf2d.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
	ismbf2d.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
Assertion	ismbf2d	⊢ ( 𝜑 → 𝐹 ∈ MblFn )

Proof

Step	Hyp	Ref	Expression
1		ismbf2d.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
2		ismbf2d.2	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
3		ismbf2d.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
4		ismbf2d.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
5		elxr	⊢ ( 𝑥 ∈ ℝ* ↔ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) )
6		oveq1	⊢ ( 𝑥 = +∞ → ( 𝑥 (,) +∞ ) = ( +∞ (,) +∞ ) )
7		iooid	⊢ ( +∞ (,) +∞ ) = ∅
8	6 7	eqtrdi	⊢ ( 𝑥 = +∞ → ( 𝑥 (,) +∞ ) = ∅ )
9	8	imaeq2d	⊢ ( 𝑥 = +∞ → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) = ( ◡ 𝐹 “ ∅ ) )
10		ima0	⊢ ( ◡ 𝐹 “ ∅ ) = ∅
11		0mbl	⊢ ∅ ∈ dom vol
12	10 11	eqeltri	⊢ ( ◡ 𝐹 “ ∅ ) ∈ dom vol
13	9 12	eqeltrdi	⊢ ( 𝑥 = +∞ → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = +∞ ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
15		fimacnv	⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( ◡ 𝐹 “ ℝ ) = 𝐴 )
16	1 15	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ ℝ ) = 𝐴 )
17	16 2	eqeltrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ ℝ ) ∈ dom vol )
18		oveq1	⊢ ( 𝑥 = -∞ → ( 𝑥 (,) +∞ ) = ( -∞ (,) +∞ ) )
19		ioomax	⊢ ( -∞ (,) +∞ ) = ℝ
20	18 19	eqtrdi	⊢ ( 𝑥 = -∞ → ( 𝑥 (,) +∞ ) = ℝ )
21	20	imaeq2d	⊢ ( 𝑥 = -∞ → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) = ( ◡ 𝐹 “ ℝ ) )
22	21	eleq1d	⊢ ( 𝑥 = -∞ → ( ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ↔ ( ◡ 𝐹 “ ℝ ) ∈ dom vol ) )
23	17 22	syl5ibrcom	⊢ ( 𝜑 → ( 𝑥 = -∞ → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ) )
24	23	imp	⊢ ( ( 𝜑 ∧ 𝑥 = -∞ ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
25	3 14 24	3jaodan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
26	5 25	sylan2b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
27		oveq2	⊢ ( 𝑥 = +∞ → ( -∞ (,) 𝑥 ) = ( -∞ (,) +∞ ) )
28	27 19	eqtrdi	⊢ ( 𝑥 = +∞ → ( -∞ (,) 𝑥 ) = ℝ )
29	28	imaeq2d	⊢ ( 𝑥 = +∞ → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) = ( ◡ 𝐹 “ ℝ ) )
30	29	eleq1d	⊢ ( 𝑥 = +∞ → ( ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol ↔ ( ◡ 𝐹 “ ℝ ) ∈ dom vol ) )
31	17 30	syl5ibrcom	⊢ ( 𝜑 → ( 𝑥 = +∞ → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol ) )
32	31	imp	⊢ ( ( 𝜑 ∧ 𝑥 = +∞ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
33		oveq2	⊢ ( 𝑥 = -∞ → ( -∞ (,) 𝑥 ) = ( -∞ (,) -∞ ) )
34		iooid	⊢ ( -∞ (,) -∞ ) = ∅
35	33 34	eqtrdi	⊢ ( 𝑥 = -∞ → ( -∞ (,) 𝑥 ) = ∅ )
36	35	imaeq2d	⊢ ( 𝑥 = -∞ → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) = ( ◡ 𝐹 “ ∅ ) )
37	36 12	eqeltrdi	⊢ ( 𝑥 = -∞ → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = -∞ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
39	4 32 38	3jaodan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
40	5 39	sylan2b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
41	1 26 40	ismbfd	⊢ ( 𝜑 → 𝐹 ∈ MblFn )