Metamath Proof Explorer

Theorem ismbf3d

Description: Simplified form of ismbfd . (Contributed by Mario Carneiro, 18-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 ismbf3d.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
2 ismbf3d.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
3 fimacnv ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( ◡ 𝐹 “ ℝ ) = 𝐴 )
4 1 3 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ℝ ) = 𝐴 )
5 imaiun ⊢ ( ◡ 𝐹 “ ∪ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ ) ) = ∪ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) )
6 ioossre ⊢ ( - 𝑦 (,) +∞ ) ⊆ ℝ
7 6 rgenw ⊢ ∀ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ ) ⊆ ℝ
8 iunss ⊢ ( ∪ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ ) ⊆ ℝ ↔ ∀ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ ) ⊆ ℝ )
9 7 8 mpbir ⊢ ∪ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ ) ⊆ ℝ
10 renegcl ⊢ ( 𝑧 ∈ ℝ → - 𝑧 ∈ ℝ )
11 arch ⊢ ( - 𝑧 ∈ ℝ → ∃ 𝑦 ∈ ℕ - 𝑧 < 𝑦 )
12 10 11 syl ⊢ ( 𝑧 ∈ ℝ → ∃ 𝑦 ∈ ℕ - 𝑧 < 𝑦 )
13 simpl ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ ) → 𝑧 ∈ ℝ )
14 13 biantrurd ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ ) → ( - 𝑦 < 𝑧 ↔ ( 𝑧 ∈ ℝ ∧ - 𝑦 < 𝑧 ) ) )
15 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
16 ltnegcon1 ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( - 𝑧 < 𝑦 ↔ - 𝑦 < 𝑧 ) )
17 15 16 sylan2 ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ ) → ( - 𝑧 < 𝑦 ↔ - 𝑦 < 𝑧 ) )
18 15 adantl ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℝ )
19 18 renegcld ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ ) → - 𝑦 ∈ ℝ )
20 19 rexrd ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ ) → - 𝑦 ∈ ℝ* )
21 elioopnf ⊢ ( - 𝑦 ∈ ℝ* → ( 𝑧 ∈ ( - 𝑦 (,) +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ - 𝑦 < 𝑧 ) ) )
22 20 21 syl ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ ) → ( 𝑧 ∈ ( - 𝑦 (,) +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ - 𝑦 < 𝑧 ) ) )
23 14 17 22 3bitr4d ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ ) → ( - 𝑧 < 𝑦 ↔ 𝑧 ∈ ( - 𝑦 (,) +∞ ) ) )
24 23 rexbidva ⊢ ( 𝑧 ∈ ℝ → ( ∃ 𝑦 ∈ ℕ - 𝑧 < 𝑦 ↔ ∃ 𝑦 ∈ ℕ 𝑧 ∈ ( - 𝑦 (,) +∞ ) ) )
25 12 24 mpbid ⊢ ( 𝑧 ∈ ℝ → ∃ 𝑦 ∈ ℕ 𝑧 ∈ ( - 𝑦 (,) +∞ ) )
26 eliun ⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ ) ↔ ∃ 𝑦 ∈ ℕ 𝑧 ∈ ( - 𝑦 (,) +∞ ) )
27 25 26 sylibr ⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ∪ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ ) )
28 27 ssriv ⊢ ℝ ⊆ ∪ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ )
29 9 28 eqssi ⊢ ∪ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ ) = ℝ
30 29 imaeq2i ⊢ ( ◡ 𝐹 “ ∪ 𝑦 ∈ ℕ ( - 𝑦 (,) +∞ ) ) = ( ◡ 𝐹 “ ℝ )
31 5 30 eqtr3i ⊢ ∪ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) ) = ( ◡ 𝐹 “ ℝ )
32 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
33 15 renegcld ⊢ ( 𝑦 ∈ ℕ → - 𝑦 ∈ ℝ )
34 oveq1 ⊢ ( 𝑥 = - 𝑦 → ( 𝑥 (,) +∞ ) = ( - 𝑦 (,) +∞ ) )
35 34 imaeq2d ⊢ ( 𝑥 = - 𝑦 → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) = ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) ) )
36 35 eleq1d ⊢ ( 𝑥 = - 𝑦 → ( ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ↔ ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol ) )
37 36 rspccva ⊢ ( ( ∀ 𝑥 ∈ ℝ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ∧ - 𝑦 ∈ ℝ ) → ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol )
38 32 33 37 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol )
39 38 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol )
40 iunmbl ⊢ ( ∀ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol → ∪ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol )
41 39 40 syl ⊢ ( 𝜑 → ∪ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol )
42 31 41 eqeltrrid ⊢ ( 𝜑 → ( ◡ 𝐹 “ ℝ ) ∈ dom vol )
43 4 42 eqeltrrd ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
44 imaiun ⊢ ( ◡ 𝐹 “ ∪ 𝑦 ∈ ℕ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) = ∪ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) )
45 eliun ⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ ℕ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℕ 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) )
46 3simpb ⊢ ( ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ) )
47 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ) → 𝑧 ∈ ℝ )
48 nnrp ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ+ )
49 48 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ) → 𝑦 ∈ ℝ+ )
50 49 rpreccld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ) → ( 1 / 𝑦 ) ∈ ℝ+ )
51 47 50 ltsubrpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ) → ( 𝑧 − ( 1 / 𝑦 ) ) < 𝑧 )
52 simprr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ) → 𝑥 ∈ ℝ )
53 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ )
54 nnrecre ⊢ ( 𝑦 ∈ ℕ → ( 1 / 𝑦 ) ∈ ℝ )
55 resubcl ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 1 / 𝑦 ) ∈ ℝ ) → ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ )
56 53 54 55 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ )
57 56 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ) → ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ )
58 lelttr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ∧ ( 𝑧 − ( 1 / 𝑦 ) ) < 𝑧 ) → 𝑥 < 𝑧 ) )
59 52 57 47 58 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ∧ ( 𝑧 − ( 1 / 𝑦 ) ) < 𝑧 ) → 𝑥 < 𝑧 ) )
60 51 59 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ) → ( 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) → 𝑥 < 𝑧 ) )
61 60 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) → 𝑥 < 𝑧 ) )
62 61 imdistanda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) )
63 46 62 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) )
64 mnfxr ⊢ -∞ ∈ ℝ*
65 elioc2 ⊢ ( ( -∞ ∈ ℝ* ∧ ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ ) → ( 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ) ) )
66 64 56 65 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ) ) )
67 rexr ⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℝ* )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ* )
69 elioomnf ⊢ ( 𝑧 ∈ ℝ* → ( 𝑥 ∈ ( -∞ (,) 𝑧 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) )
70 68 69 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( 𝑥 ∈ ( -∞ (,) 𝑧 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) )
71 70 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( 𝑥 ∈ ( -∞ (,) 𝑧 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) )
72 63 66 71 3imtr4d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) → 𝑥 ∈ ( -∞ (,) 𝑧 ) ) )
73 72 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℕ 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) → 𝑥 ∈ ( -∞ (,) 𝑧 ) ) )
74 73 70 sylibd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℕ 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) )
75 simprl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) → 𝑥 ∈ ℝ )
76 75 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → 𝑥 ∈ ℝ )
77 76 mnfltd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → -∞ < 𝑥 )
78 56 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ )
79 54 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → ( 1 / 𝑦 ) ∈ ℝ )
80 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) → 𝑧 ∈ ℝ )
81 80 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → 𝑧 ∈ ℝ )
82 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) )
83 79 81 76 82 ltsub13d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → 𝑥 < ( 𝑧 − ( 1 / 𝑦 ) ) )
84 76 78 83 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) )
85 66 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → ( 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ) ) )
86 76 77 84 85 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) ) ) → 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) )
87 80 75 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) → ( 𝑧 − 𝑥 ) ∈ ℝ )
88 simprr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) → 𝑥 < 𝑧 )
89 75 80 posdifd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) → ( 𝑥 < 𝑧 ↔ 0 < ( 𝑧 − 𝑥 ) ) )
90 88 89 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) → 0 < ( 𝑧 − 𝑥 ) )
91 nnrecl ⊢ ( ( ( 𝑧 − 𝑥 ) ∈ ℝ ∧ 0 < ( 𝑧 − 𝑥 ) ) → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) )
92 87 90 91 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < ( 𝑧 − 𝑥 ) )
93 86 92 reximddv ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) → ∃ 𝑦 ∈ ℕ 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) )
94 93 ex ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) → ∃ 𝑦 ∈ ℕ 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) )
95 74 94 impbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℕ 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝑧 ) ) )
96 95 70 bitr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℕ 𝑥 ∈ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ↔ 𝑥 ∈ ( -∞ (,) 𝑧 ) ) )
97 45 96 syl5bb ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( 𝑥 ∈ ∪ 𝑦 ∈ ℕ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ↔ 𝑥 ∈ ( -∞ (,) 𝑧 ) ) )
98 97 eqrdv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ∪ 𝑦 ∈ ℕ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) = ( -∞ (,) 𝑧 ) )
99 98 imaeq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ◡ 𝐹 “ ∪ 𝑦 ∈ ℕ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) = ( ◡ 𝐹 “ ( -∞ (,) 𝑧 ) ) )
100 44 99 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ∪ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) = ( ◡ 𝐹 “ ( -∞ (,) 𝑧 ) ) )
101 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → 𝐹 : 𝐴 ⟶ ℝ )
102 ffun ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → Fun 𝐹 )
103 funcnvcnv ⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
104 imadif ⊢ ( Fun ◡ ◡ 𝐹 → ( ◡ 𝐹 “ ( ℝ ∖ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ) = ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ) )
105 101 102 103 104 4syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ◡ 𝐹 “ ( ℝ ∖ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ) = ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ) )
106 64 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → -∞ ∈ ℝ* )
107 56 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ* )
108 pnfxr ⊢ +∞ ∈ ℝ*
109 108 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → +∞ ∈ ℝ* )
110 56 mnfltd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → -∞ < ( 𝑧 − ( 1 / 𝑦 ) ) )
111 56 ltpnfd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( 𝑧 − ( 1 / 𝑦 ) ) < +∞ )
112 df-ioc ⊢ (,] = ( 𝑢 ∈ ℝ* , 𝑣 ∈ ℝ* ↦ { 𝑤 ∈ ℝ* ∣ ( 𝑢 < 𝑤 ∧ 𝑤 ≤ 𝑣 ) } )
113 df-ioo ⊢ (,) = ( 𝑢 ∈ ℝ* , 𝑣 ∈ ℝ* ↦ { 𝑤 ∈ ℝ* ∣ ( 𝑢 < 𝑤 ∧ 𝑤 < 𝑣 ) } )
114 xrltnle ⊢ ( ( ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( 𝑧 − ( 1 / 𝑦 ) ) < 𝑥 ↔ ¬ 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ) )
115 xrlelttr ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝑥 ≤ ( 𝑧 − ( 1 / 𝑦 ) ) ∧ ( 𝑧 − ( 1 / 𝑦 ) ) < +∞ ) → 𝑥 < +∞ ) )
116 xrlttr ⊢ ( ( -∞ ∈ ℝ* ∧ ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( -∞ < ( 𝑧 − ( 1 / 𝑦 ) ) ∧ ( 𝑧 − ( 1 / 𝑦 ) ) < 𝑥 ) → -∞ < 𝑥 ) )
117 112 113 114 113 115 116 ixxun ⊢ ( ( ( -∞ ∈ ℝ* ∧ ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ < ( 𝑧 − ( 1 / 𝑦 ) ) ∧ ( 𝑧 − ( 1 / 𝑦 ) ) < +∞ ) ) → ( ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ∪ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) = ( -∞ (,) +∞ ) )
118 106 107 109 110 111 117 syl32anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ∪ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) = ( -∞ (,) +∞ ) )
119 uncom ⊢ ( ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ∪ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) = ( ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ∪ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) )
120 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
121 118 119 120 3eqtr3g ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ∪ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) = ℝ )
122 ioossre ⊢ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ⊆ ℝ
123 incom ⊢ ( ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ∩ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) = ( ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ∩ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) )
124 112 113 114 ixxdisj ⊢ ( ( -∞ ∈ ℝ* ∧ ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ∩ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) = ∅ )
125 64 108 124 mp3an13 ⊢ ( ( 𝑧 − ( 1 / 𝑦 ) ) ∈ ℝ* → ( ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ∩ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) = ∅ )
126 107 125 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ∩ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) = ∅ )
127 123 126 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ∩ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) = ∅ )
128 uneqdifeq ⊢ ( ( ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ⊆ ℝ ∧ ( ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ∩ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) = ∅ ) → ( ( ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ∪ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) = ℝ ↔ ( ℝ ∖ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) = ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) )
129 122 127 128 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ∪ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) = ℝ ↔ ( ℝ ∖ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) = ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) )
130 121 129 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ℝ ∖ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) = ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) )
131 130 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ◡ 𝐹 “ ( ℝ ∖ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ) = ( ◡ 𝐹 “ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) )
132 105 131 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ) = ( ◡ 𝐹 “ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) )
133 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ◡ 𝐹 “ ℝ ) ∈ dom vol )
134 oveq1 ⊢ ( 𝑥 = ( 𝑧 − ( 1 / 𝑦 ) ) → ( 𝑥 (,) +∞ ) = ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) )
135 134 imaeq2d ⊢ ( 𝑥 = ( 𝑧 − ( 1 / 𝑦 ) ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) = ( ◡ 𝐹 “ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) )
136 135 eleq1d ⊢ ( 𝑥 = ( 𝑧 − ( 1 / 𝑦 ) ) → ( ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ↔ ( ◡ 𝐹 “ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ∈ dom vol ) )
137 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
138 136 137 56 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ◡ 𝐹 “ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ∈ dom vol )
139 difmbl ⊢ ( ( ( ◡ 𝐹 “ ℝ ) ∈ dom vol ∧ ( ◡ 𝐹 “ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ∈ dom vol ) → ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ) ∈ dom vol )
140 133 138 139 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ( 𝑧 − ( 1 / 𝑦 ) ) (,) +∞ ) ) ) ∈ dom vol )
141 132 140 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ◡ 𝐹 “ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) ∈ dom vol )
142 141 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ∀ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) ∈ dom vol )
143 iunmbl ⊢ ( ∀ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) ∈ dom vol → ∪ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) ∈ dom vol )
144 142 143 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ∪ 𝑦 ∈ ℕ ( ◡ 𝐹 “ ( -∞ (,] ( 𝑧 − ( 1 / 𝑦 ) ) ) ) ∈ dom vol )
145 100 144 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑧 ) ) ∈ dom vol )
146 145 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑧 ) ) ∈ dom vol )
147 oveq2 ⊢ ( 𝑧 = 𝑥 → ( -∞ (,) 𝑧 ) = ( -∞ (,) 𝑥 ) )
148 147 imaeq2d ⊢ ( 𝑧 = 𝑥 → ( ◡ 𝐹 “ ( -∞ (,) 𝑧 ) ) = ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) )
149 148 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ( ◡ 𝐹 “ ( -∞ (,) 𝑧 ) ) ∈ dom vol ↔ ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol ) )
150 149 cbvralvw ⊢ ( ∀ 𝑧 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑧 ) ) ∈ dom vol ↔ ∀ 𝑥 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
151 146 150 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
152 151 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
153 1 43 2 152 ismbf2d ⊢ ( 𝜑 → 𝐹 ∈ MblFn )