This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )