Theorem ismbfd

Description: Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d . (Contributed by Mario Carneiro, 18-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ismbfd.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
2		ismbfd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
3		ismbfd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
4		ioof	⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
5		ffn	⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
6		ovelrn	⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝑧 ∈ ran (,) ↔ ∃ 𝑥 ∈ ℝ* ∃ 𝑦 ∈ ℝ* 𝑧 = ( 𝑥 (,) 𝑦 ) ) )
7	4 5 6	mp2b	⊢ ( 𝑧 ∈ ran (,) ↔ ∃ 𝑥 ∈ ℝ* ∃ 𝑦 ∈ ℝ* 𝑧 = ( 𝑥 (,) 𝑦 ) )
8		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → 𝑥 ∈ ℝ* )
9		pnfxr	⊢ +∞ ∈ ℝ*
10	9	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → +∞ ∈ ℝ* )
11		mnfxr	⊢ -∞ ∈ ℝ*
12	11	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → -∞ ∈ ℝ* )
13		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → 𝑦 ∈ ℝ* )
14		iooin	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ( 𝑥 (,) +∞ ) ∩ ( -∞ (,) 𝑦 ) ) = ( if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) (,) if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) ) )
15	8 10 12 13 14	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ( 𝑥 (,) +∞ ) ∩ ( -∞ (,) 𝑦 ) ) = ( if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) (,) if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) ) )
16		ifcl	⊢ ( ( -∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) ∈ ℝ* )
17	11 8 16	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) ∈ ℝ* )
18		mnfle	⊢ ( 𝑥 ∈ ℝ* → -∞ ≤ 𝑥 )
19		xrleid	⊢ ( 𝑥 ∈ ℝ* → 𝑥 ≤ 𝑥 )
20		breq1	⊢ ( -∞ = if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) → ( -∞ ≤ 𝑥 ↔ if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) ≤ 𝑥 ) )
21		breq1	⊢ ( 𝑥 = if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) → ( 𝑥 ≤ 𝑥 ↔ if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) ≤ 𝑥 ) )
22	20 21	ifboth	⊢ ( ( -∞ ≤ 𝑥 ∧ 𝑥 ≤ 𝑥 ) → if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) ≤ 𝑥 )
23	18 19 22	syl2anc	⊢ ( 𝑥 ∈ ℝ* → if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) ≤ 𝑥 )
24	23	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) ≤ 𝑥 )
25		xrmax1	⊢ ( ( 𝑥 ∈ ℝ* ∧ -∞ ∈ ℝ* ) → 𝑥 ≤ if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) )
26	8 11 25	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → 𝑥 ≤ if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) )
27	17 8 24 26	xrletrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) = 𝑥 )
28		ifcl	⊢ ( ( +∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) ∈ ℝ* )
29	9 13 28	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) ∈ ℝ* )
30		xrmin2	⊢ ( ( +∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) ≤ 𝑦 )
31	9 13 30	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) ≤ 𝑦 )
32		pnfge	⊢ ( 𝑦 ∈ ℝ* → 𝑦 ≤ +∞ )
33		xrleid	⊢ ( 𝑦 ∈ ℝ* → 𝑦 ≤ 𝑦 )
34		breq2	⊢ ( +∞ = if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) → ( 𝑦 ≤ +∞ ↔ 𝑦 ≤ if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) ) )
35		breq2	⊢ ( 𝑦 = if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) → ( 𝑦 ≤ 𝑦 ↔ 𝑦 ≤ if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) ) )
36	34 35	ifboth	⊢ ( ( 𝑦 ≤ +∞ ∧ 𝑦 ≤ 𝑦 ) → 𝑦 ≤ if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) )
37	32 33 36	syl2anc	⊢ ( 𝑦 ∈ ℝ* → 𝑦 ≤ if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) )
38	37	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → 𝑦 ≤ if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) )
39	29 13 31 38	xrletrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) = 𝑦 )
40	27 39	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( if ( 𝑥 ≤ -∞ , -∞ , 𝑥 ) (,) if ( +∞ ≤ 𝑦 , +∞ , 𝑦 ) ) = ( 𝑥 (,) 𝑦 ) )
41	15 40	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ( 𝑥 (,) +∞ ) ∩ ( -∞ (,) 𝑦 ) ) = ( 𝑥 (,) 𝑦 ) )
42	41	imaeq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( ( 𝑥 (,) +∞ ) ∩ ( -∞ (,) 𝑦 ) ) ) = ( ◡ 𝐹 “ ( 𝑥 (,) 𝑦 ) ) )
43	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → 𝐹 : 𝐴 ⟶ ℝ )
44	43	ffund	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → Fun 𝐹 )
45		inpreima	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ( 𝑥 (,) +∞ ) ∩ ( -∞ (,) 𝑦 ) ) ) = ( ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ) )
46	44 45	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( ( 𝑥 (,) +∞ ) ∩ ( -∞ (,) 𝑦 ) ) ) = ( ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ) )
47	42 46	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( 𝑥 (,) 𝑦 ) ) = ( ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ) )
48	2	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
49	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ* ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
50		oveq2	⊢ ( 𝑥 = 𝑦 → ( -∞ (,) 𝑥 ) = ( -∞ (,) 𝑦 ) )
51	50	imaeq2d	⊢ ( 𝑥 = 𝑦 → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) = ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) )
52	51	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol ↔ ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol ) )
53	52	rspccva	⊢ ( ( ∀ 𝑥 ∈ ℝ* ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol ∧ 𝑦 ∈ ℝ* ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
54	49 53	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
55	54	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
56		inmbl	⊢ ( ( ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ∧ ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol ) → ( ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ) ∈ dom vol )
57	48 55 56	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ) ∈ dom vol )
58	47 57	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( 𝑥 (,) 𝑦 ) ) ∈ dom vol )
59		imaeq2	⊢ ( 𝑧 = ( 𝑥 (,) 𝑦 ) → ( ◡ 𝐹 “ 𝑧 ) = ( ◡ 𝐹 “ ( 𝑥 (,) 𝑦 ) ) )
60	59	eleq1d	⊢ ( 𝑧 = ( 𝑥 (,) 𝑦 ) → ( ( ◡ 𝐹 “ 𝑧 ) ∈ dom vol ↔ ( ◡ 𝐹 “ ( 𝑥 (,) 𝑦 ) ) ∈ dom vol ) )
61	58 60	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( 𝑧 = ( 𝑥 (,) 𝑦 ) → ( ◡ 𝐹 “ 𝑧 ) ∈ dom vol ) )
62	61	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ* ∃ 𝑦 ∈ ℝ* 𝑧 = ( 𝑥 (,) 𝑦 ) → ( ◡ 𝐹 “ 𝑧 ) ∈ dom vol ) )
63	7 62	biimtrid	⊢ ( 𝜑 → ( 𝑧 ∈ ran (,) → ( ◡ 𝐹 “ 𝑧 ) ∈ dom vol ) )
64	63	ralrimiv	⊢ ( 𝜑 → ∀ 𝑧 ∈ ran (,) ( ◡ 𝐹 “ 𝑧 ) ∈ dom vol )
65		ismbf	⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝐹 ∈ MblFn ↔ ∀ 𝑧 ∈ ran (,) ( ◡ 𝐹 “ 𝑧 ) ∈ dom vol ) )
66	1 65	syl	⊢ ( 𝜑 → ( 𝐹 ∈ MblFn ↔ ∀ 𝑧 ∈ ran (,) ( ◡ 𝐹 “ 𝑧 ) ∈ dom vol ) )
67	64 66	mpbird	⊢ ( 𝜑 → 𝐹 ∈ MblFn )