| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ismbf3d.1 | . 2
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) | 
| 2 |  | fimacnv 6757 | . . . 4
⊢ (𝐹:𝐴⟶ℝ → (◡𝐹 “ ℝ) = 𝐴) | 
| 3 | 1, 2 | syl 17 | . . 3
⊢ (𝜑 → (◡𝐹 “ ℝ) = 𝐴) | 
| 4 |  | imaiun 7266 | . . . . 5
⊢ (◡𝐹 “ ∪
𝑦 ∈ ℕ (-𝑦(,)+∞)) = ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) | 
| 5 |  | ioossre 13449 | . . . . . . . . 9
⊢ (-𝑦(,)+∞) ⊆
ℝ | 
| 6 | 5 | rgenw 3064 | . . . . . . . 8
⊢
∀𝑦 ∈
ℕ (-𝑦(,)+∞)
⊆ ℝ | 
| 7 |  | iunss 5044 | . . . . . . . 8
⊢ (∪ 𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ ↔
∀𝑦 ∈ ℕ
(-𝑦(,)+∞) ⊆
ℝ) | 
| 8 | 6, 7 | mpbir 231 | . . . . . . 7
⊢ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞) ⊆ ℝ | 
| 9 |  | renegcl 11573 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℝ → -𝑧 ∈
ℝ) | 
| 10 |  | arch 12525 | . . . . . . . . . . 11
⊢ (-𝑧 ∈ ℝ →
∃𝑦 ∈ ℕ
-𝑧 < 𝑦) | 
| 11 | 9, 10 | syl 17 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℝ →
∃𝑦 ∈ ℕ
-𝑧 < 𝑦) | 
| 12 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → 𝑧 ∈
ℝ) | 
| 13 | 12 | biantrurd 532 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (-𝑦 < 𝑧 ↔ (𝑧 ∈ ℝ ∧ -𝑦 < 𝑧))) | 
| 14 |  | nnre 12274 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) | 
| 15 |  | ltnegcon1 11765 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-𝑧 < 𝑦 ↔ -𝑦 < 𝑧)) | 
| 16 | 14, 15 | sylan2 593 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (-𝑧 < 𝑦 ↔ -𝑦 < 𝑧)) | 
| 17 | 14 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℝ) | 
| 18 | 17 | renegcld 11691 | . . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → -𝑦 ∈
ℝ) | 
| 19 | 18 | rexrd 11312 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → -𝑦 ∈
ℝ*) | 
| 20 |  | elioopnf 13484 | . . . . . . . . . . . . 13
⊢ (-𝑦 ∈ ℝ*
→ (𝑧 ∈ (-𝑦(,)+∞) ↔ (𝑧 ∈ ℝ ∧ -𝑦 < 𝑧))) | 
| 21 | 19, 20 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (𝑧 ∈ (-𝑦(,)+∞) ↔ (𝑧 ∈ ℝ ∧ -𝑦 < 𝑧))) | 
| 22 | 13, 16, 21 | 3bitr4d 311 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℕ) → (-𝑧 < 𝑦 ↔ 𝑧 ∈ (-𝑦(,)+∞))) | 
| 23 | 22 | rexbidva 3176 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℝ →
(∃𝑦 ∈ ℕ
-𝑧 < 𝑦 ↔ ∃𝑦 ∈ ℕ 𝑧 ∈ (-𝑦(,)+∞))) | 
| 24 | 11, 23 | mpbid 232 | . . . . . . . . 9
⊢ (𝑧 ∈ ℝ →
∃𝑦 ∈ ℕ
𝑧 ∈ (-𝑦(,)+∞)) | 
| 25 |  | eliun 4994 | . . . . . . . . 9
⊢ (𝑧 ∈ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞) ↔ ∃𝑦 ∈ ℕ 𝑧 ∈ (-𝑦(,)+∞)) | 
| 26 | 24, 25 | sylibr 234 | . . . . . . . 8
⊢ (𝑧 ∈ ℝ → 𝑧 ∈ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞)) | 
| 27 | 26 | ssriv 3986 | . . . . . . 7
⊢ ℝ
⊆ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞) | 
| 28 | 8, 27 | eqssi 3999 | . . . . . 6
⊢ ∪ 𝑦 ∈ ℕ (-𝑦(,)+∞) = ℝ | 
| 29 | 28 | imaeq2i 6075 | . . . . 5
⊢ (◡𝐹 “ ∪
𝑦 ∈ ℕ (-𝑦(,)+∞)) = (◡𝐹 “ ℝ) | 
| 30 | 4, 29 | eqtr3i 2766 | . . . 4
⊢ ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) = (◡𝐹 “ ℝ) | 
| 31 |  | ismbf3d.2 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom
vol) | 
| 32 | 31 | ralrimiva 3145 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ ℝ (◡𝐹 “ (𝑥(,)+∞)) ∈ dom
vol) | 
| 33 | 14 | renegcld 11691 | . . . . . . 7
⊢ (𝑦 ∈ ℕ → -𝑦 ∈
ℝ) | 
| 34 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑥 = -𝑦 → (𝑥(,)+∞) = (-𝑦(,)+∞)) | 
| 35 | 34 | imaeq2d 6077 | . . . . . . . . 9
⊢ (𝑥 = -𝑦 → (◡𝐹 “ (𝑥(,)+∞)) = (◡𝐹 “ (-𝑦(,)+∞))) | 
| 36 | 35 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑥 = -𝑦 → ((◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol ↔ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom
vol)) | 
| 37 | 36 | rspccva 3620 | . . . . . . 7
⊢
((∀𝑥 ∈
ℝ (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol ∧ -𝑦 ∈ ℝ) → (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom
vol) | 
| 38 | 32, 33, 37 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom
vol) | 
| 39 | 38 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom
vol) | 
| 40 |  | iunmbl 25589 | . . . . 5
⊢
(∀𝑦 ∈
ℕ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom vol → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom
vol) | 
| 41 | 39, 40 | syl 17 | . . . 4
⊢ (𝜑 → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-𝑦(,)+∞)) ∈ dom
vol) | 
| 42 | 30, 41 | eqeltrrid 2845 | . . 3
⊢ (𝜑 → (◡𝐹 “ ℝ) ∈ dom
vol) | 
| 43 | 3, 42 | eqeltrrd 2841 | . 2
⊢ (𝜑 → 𝐴 ∈ dom vol) | 
| 44 |  | imaiun 7266 | . . . . . . 7
⊢ (◡𝐹 “ ∪
𝑦 ∈ ℕ
(-∞(,](𝑧 − (1 /
𝑦)))) = ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) | 
| 45 |  | eliun 4994 | . . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦))) ↔ ∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦)))) | 
| 46 |  | 3simpb 1149 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ -∞
< 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦)))) | 
| 47 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → 𝑧 ∈ ℝ) | 
| 48 |  | nnrp 13047 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ+) | 
| 49 | 48 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → 𝑦 ∈ ℝ+) | 
| 50 | 49 | rpreccld 13088 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (1 / 𝑦) ∈
ℝ+) | 
| 51 | 47, 50 | ltsubrpd 13110 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (𝑧 − (1 / 𝑦)) < 𝑧) | 
| 52 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → 𝑥 ∈ ℝ) | 
| 53 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℝ) | 
| 54 |  | nnrecre 12309 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℕ → (1 /
𝑦) ∈
ℝ) | 
| 55 |  | resubcl 11574 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℝ ∧ (1 / 𝑦) ∈ ℝ) → (𝑧 − (1 / 𝑦)) ∈ ℝ) | 
| 56 | 53, 54, 55 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 − (1 / 𝑦)) ∈ ℝ) | 
| 57 | 56 | adantrr 717 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (𝑧 − (1 / 𝑦)) ∈ ℝ) | 
| 58 |  | lelttr 11352 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 ≤ (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < 𝑧) → 𝑥 < 𝑧)) | 
| 59 | 52, 57, 47, 58 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → ((𝑥 ≤ (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < 𝑧) → 𝑥 < 𝑧)) | 
| 60 | 51, 59 | mpan2d 694 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑥 ∈ ℝ)) → (𝑥 ≤ (𝑧 − (1 / 𝑦)) → 𝑥 < 𝑧)) | 
| 61 | 60 | anassrs 467 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ≤ (𝑧 − (1 / 𝑦)) → 𝑥 < 𝑧)) | 
| 62 | 61 | imdistanda 571 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑥 ∈ ℝ ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧))) | 
| 63 | 46, 62 | syl5 34 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧))) | 
| 64 |  | mnfxr 11319 | . . . . . . . . . . . . . . . 16
⊢ -∞
∈ ℝ* | 
| 65 |  | elioc2 13451 | . . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))))) | 
| 66 | 64, 56, 65 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))))) | 
| 67 |  | rexr 11308 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℝ → 𝑧 ∈
ℝ*) | 
| 68 | 67 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℝ*) | 
| 69 |  | elioomnf 13485 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℝ*
→ (𝑥 ∈
(-∞(,)𝑧) ↔
(𝑥 ∈ ℝ ∧
𝑥 < 𝑧))) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑥 ∈ (-∞(,)𝑧) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧))) | 
| 71 | 70 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ (-∞(,)𝑧) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧))) | 
| 72 | 63, 66, 71 | 3imtr4d 294 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) → 𝑥 ∈ (-∞(,)𝑧))) | 
| 73 | 72 | rexlimdva 3154 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) → 𝑥 ∈ (-∞(,)𝑧))) | 
| 74 | 73, 70 | sylibd 239 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) → (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧))) | 
| 75 |  | simprl 770 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 𝑥 ∈ ℝ) | 
| 76 | 75 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑥 ∈ ℝ) | 
| 77 | 76 | mnfltd 13167 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → -∞ < 𝑥) | 
| 78 | 56 | ad2ant2r 747 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → (𝑧 − (1 / 𝑦)) ∈ ℝ) | 
| 79 | 54 | ad2antrl 728 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → (1 / 𝑦) ∈ ℝ) | 
| 80 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 𝑧 ∈ ℝ) | 
| 81 | 80 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑧 ∈ ℝ) | 
| 82 |  | simprr 772 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → (1 / 𝑦) < (𝑧 − 𝑥)) | 
| 83 | 79, 81, 76, 82 | ltsub13d 11870 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑥 < (𝑧 − (1 / 𝑦))) | 
| 84 | 76, 78, 83 | ltled 11410 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑥 ≤ (𝑧 − (1 / 𝑦))) | 
| 85 | 66 | ad2ant2r 747 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → (𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ (𝑧 − (1 / 𝑦))))) | 
| 86 | 76, 77, 84, 85 | mpbir3and 1342 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < (𝑧 − 𝑥))) → 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦)))) | 
| 87 | 80, 75 | resubcld 11692 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → (𝑧 − 𝑥) ∈ ℝ) | 
| 88 |  | simprr 772 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 𝑥 < 𝑧) | 
| 89 | 75, 80 | posdifd 11851 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → (𝑥 < 𝑧 ↔ 0 < (𝑧 − 𝑥))) | 
| 90 | 88, 89 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → 0 < (𝑧 − 𝑥)) | 
| 91 |  | nnrecl 12526 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 − 𝑥) ∈ ℝ ∧ 0 < (𝑧 − 𝑥)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝑧 − 𝑥)) | 
| 92 | 87, 90, 91 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝑧 − 𝑥)) | 
| 93 | 86, 92 | reximddv 3170 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧)) → ∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦)))) | 
| 94 | 93 | ex 412 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ((𝑥 ∈ ℝ ∧ 𝑥 < 𝑧) → ∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))))) | 
| 95 | 74, 94 | impbid 212 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝑧))) | 
| 96 | 95, 70 | bitr4d 282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑦 ∈ ℕ 𝑥 ∈ (-∞(,](𝑧 − (1 / 𝑦))) ↔ 𝑥 ∈ (-∞(,)𝑧))) | 
| 97 | 45, 96 | bitrid 283 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑥 ∈ ∪
𝑦 ∈ ℕ
(-∞(,](𝑧 − (1 /
𝑦))) ↔ 𝑥 ∈ (-∞(,)𝑧))) | 
| 98 | 97 | eqrdv 2734 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∪ 𝑦 ∈ ℕ (-∞(,](𝑧 − (1 / 𝑦))) = (-∞(,)𝑧)) | 
| 99 | 98 | imaeq2d 6077 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (◡𝐹 “ ∪
𝑦 ∈ ℕ
(-∞(,](𝑧 − (1 /
𝑦)))) = (◡𝐹 “ (-∞(,)𝑧))) | 
| 100 | 44, 99 | eqtr3id 2790 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) = (◡𝐹 “ (-∞(,)𝑧))) | 
| 101 | 1 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝐹:𝐴⟶ℝ) | 
| 102 |  | ffun 6738 | . . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ℝ → Fun 𝐹) | 
| 103 |  | funcnvcnv 6632 | . . . . . . . . . . 11
⊢ (Fun
𝐹 → Fun ◡◡𝐹) | 
| 104 |  | imadif 6649 | . . . . . . . . . . 11
⊢ (Fun
◡◡𝐹 → (◡𝐹 “ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)))) | 
| 105 | 101, 102,
103, 104 | 4syl 19 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)))) | 
| 106 | 64 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → -∞ ∈
ℝ*) | 
| 107 | 56 | rexrd 11312 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 − (1 / 𝑦)) ∈
ℝ*) | 
| 108 |  | pnfxr 11316 | . . . . . . . . . . . . . . 15
⊢ +∞
∈ ℝ* | 
| 109 | 108 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → +∞ ∈
ℝ*) | 
| 110 | 56 | mnfltd 13167 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → -∞ < (𝑧 − (1 / 𝑦))) | 
| 111 | 56 | ltpnfd 13164 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 − (1 / 𝑦)) < +∞) | 
| 112 |  | df-ioc 13393 | . . . . . . . . . . . . . . 15
⊢ (,] =
(𝑢 ∈
ℝ*, 𝑣
∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 < 𝑤 ∧ 𝑤 ≤ 𝑣)}) | 
| 113 |  | df-ioo 13392 | . . . . . . . . . . . . . . 15
⊢ (,) =
(𝑢 ∈
ℝ*, 𝑣
∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 < 𝑤 ∧ 𝑤 < 𝑣)}) | 
| 114 |  | xrltnle 11329 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ 𝑥 ∈ ℝ*)
→ ((𝑧 − (1 /
𝑦)) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑧 − (1 / 𝑦)))) | 
| 115 |  | xrlelttr 13199 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ (𝑧 − (1 / 𝑦)) ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((𝑥 ≤ (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < +∞) → 𝑥 < +∞)) | 
| 116 |  | xrlttr 13183 | . . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ 𝑥 ∈ ℝ*)
→ ((-∞ < (𝑧
− (1 / 𝑦)) ∧
(𝑧 − (1 / 𝑦)) < 𝑥) → -∞ < 𝑥)) | 
| 117 | 112, 113,
114, 113, 115, 116 | ixxun 13404 | . . . . . . . . . . . . . 14
⊢
(((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-∞ < (𝑧 − (1 / 𝑦)) ∧ (𝑧 − (1 / 𝑦)) < +∞)) → ((-∞(,](𝑧 − (1 / 𝑦))) ∪ ((𝑧 − (1 / 𝑦))(,)+∞)) =
(-∞(,)+∞)) | 
| 118 | 106, 107,
109, 110, 111, 117 | syl32anc 1379 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((-∞(,](𝑧 − (1 / 𝑦))) ∪ ((𝑧 − (1 / 𝑦))(,)+∞)) =
(-∞(,)+∞)) | 
| 119 |  | uncom 4157 | . . . . . . . . . . . . 13
⊢
((-∞(,](𝑧
− (1 / 𝑦))) ∪
((𝑧 − (1 / 𝑦))(,)+∞)) = (((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) | 
| 120 |  | ioomax 13463 | . . . . . . . . . . . . 13
⊢
(-∞(,)+∞) = ℝ | 
| 121 | 118, 119,
120 | 3eqtr3g 2799 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) = ℝ) | 
| 122 |  | ioossre 13449 | . . . . . . . . . . . . 13
⊢ ((𝑧 − (1 / 𝑦))(,)+∞) ⊆
ℝ | 
| 123 |  | incom 4208 | . . . . . . . . . . . . . 14
⊢ (((𝑧 − (1 / 𝑦))(,)+∞) ∩ (-∞(,](𝑧 − (1 / 𝑦)))) = ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) | 
| 124 | 112, 113,
114 | ixxdisj 13403 | . . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ (𝑧 − (1 / 𝑦)) ∈ ℝ* ∧ +∞
∈ ℝ*) → ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) = ∅) | 
| 125 | 64, 108, 124 | mp3an13 1453 | . . . . . . . . . . . . . . 15
⊢ ((𝑧 − (1 / 𝑦)) ∈ ℝ* →
((-∞(,](𝑧 − (1
/ 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) = ∅) | 
| 126 | 107, 125 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((-∞(,](𝑧 − (1 / 𝑦))) ∩ ((𝑧 − (1 / 𝑦))(,)+∞)) = ∅) | 
| 127 | 123, 126 | eqtrid 2788 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (((𝑧 − (1 / 𝑦))(,)+∞) ∩ (-∞(,](𝑧 − (1 / 𝑦)))) = ∅) | 
| 128 |  | uneqdifeq 4492 | . . . . . . . . . . . . 13
⊢ ((((𝑧 − (1 / 𝑦))(,)+∞) ⊆ ℝ ∧ (((𝑧 − (1 / 𝑦))(,)+∞) ∩ (-∞(,](𝑧 − (1 / 𝑦)))) = ∅) → ((((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) = ℝ ↔ (ℝ ∖
((𝑧 − (1 / 𝑦))(,)+∞)) =
(-∞(,](𝑧 − (1 /
𝑦))))) | 
| 129 | 122, 127,
128 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((((𝑧 − (1 / 𝑦))(,)+∞) ∪ (-∞(,](𝑧 − (1 / 𝑦)))) = ℝ ↔ (ℝ ∖
((𝑧 − (1 / 𝑦))(,)+∞)) =
(-∞(,](𝑧 − (1 /
𝑦))))) | 
| 130 | 121, 129 | mpbid 232 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (ℝ ∖
((𝑧 − (1 / 𝑦))(,)+∞)) =
(-∞(,](𝑧 − (1 /
𝑦)))) | 
| 131 | 130 | imaeq2d 6077 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ (ℝ ∖ ((𝑧 − (1 / 𝑦))(,)+∞))) = (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦))))) | 
| 132 | 105, 131 | eqtr3d 2778 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) = (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦))))) | 
| 133 | 42 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ ℝ) ∈ dom
vol) | 
| 134 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝑧 − (1 / 𝑦)) → (𝑥(,)+∞) = ((𝑧 − (1 / 𝑦))(,)+∞)) | 
| 135 | 134 | imaeq2d 6077 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 − (1 / 𝑦)) → (◡𝐹 “ (𝑥(,)+∞)) = (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) | 
| 136 | 135 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑧 − (1 / 𝑦)) → ((◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol ↔ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)) ∈ dom
vol)) | 
| 137 | 32 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ∀𝑥 ∈ ℝ (◡𝐹 “ (𝑥(,)+∞)) ∈ dom
vol) | 
| 138 | 136, 137,
56 | rspcdva 3622 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)) ∈ dom
vol) | 
| 139 |  | difmbl 25579 | . . . . . . . . . 10
⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧
(◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞)) ∈ dom vol) →
((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) ∈ dom
vol) | 
| 140 | 133, 138,
139 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ ((𝑧 − (1 / 𝑦))(,)+∞))) ∈ dom
vol) | 
| 141 | 132, 140 | eqeltrrd 2841 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol) | 
| 142 | 141 | ralrimiva 3145 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∀𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol) | 
| 143 |  | iunmbl 25589 | . . . . . . 7
⊢
(∀𝑦 ∈
ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol) | 
| 144 | 142, 143 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∪ 𝑦 ∈ ℕ (◡𝐹 “ (-∞(,](𝑧 − (1 / 𝑦)))) ∈ dom vol) | 
| 145 | 100, 144 | eqeltrrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑧)) ∈ dom vol) | 
| 146 | 145 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑧 ∈ ℝ (◡𝐹 “ (-∞(,)𝑧)) ∈ dom vol) | 
| 147 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑧 = 𝑥 → (-∞(,)𝑧) = (-∞(,)𝑥)) | 
| 148 | 147 | imaeq2d 6077 | . . . . . 6
⊢ (𝑧 = 𝑥 → (◡𝐹 “ (-∞(,)𝑧)) = (◡𝐹 “ (-∞(,)𝑥))) | 
| 149 | 148 | eleq1d 2825 | . . . . 5
⊢ (𝑧 = 𝑥 → ((◡𝐹 “ (-∞(,)𝑧)) ∈ dom vol ↔ (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol)) | 
| 150 | 149 | cbvralvw 3236 | . . . 4
⊢
(∀𝑧 ∈
ℝ (◡𝐹 “ (-∞(,)𝑧)) ∈ dom vol ↔ ∀𝑥 ∈ ℝ (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) | 
| 151 | 146, 150 | sylib 218 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) | 
| 152 | 151 | r19.21bi 3250 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) | 
| 153 | 1, 43, 31, 152 | ismbf2d 25676 | 1
⊢ (𝜑 → 𝐹 ∈ MblFn) |