| Step | Hyp | Ref
| Expression |
| 1 | | mbfpos.1 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| 2 | 1 | fmpttd 7135 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) |
| 3 | | mbfposr.2 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) |
| 4 | | 0re 11263 |
. . . 4
⊢ 0 ∈
ℝ |
| 5 | | ifcl 4571 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
| 6 | 1, 4, 5 | sylancl 586 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
| 7 | 3, 6 | mbfdm2 25672 |
. 2
⊢ (𝜑 → 𝐴 ∈ dom vol) |
| 8 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 < 0) |
| 9 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
| 10 | 9 | lt0neg1d 11832 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 0 ↔ 0 < -𝑦)) |
| 11 | 8, 10 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 0 < -𝑦) |
| 12 | 11 | biantrurd 532 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (-𝐵 < -𝑦 ↔ (0 < -𝑦 ∧ -𝐵 < -𝑦))) |
| 13 | 1 | ad4ant14 752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| 14 | 9, 13 | ltnegd 11841 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 𝐵 ↔ -𝐵 < -𝑦)) |
| 15 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
| 16 | 13 | renegcld 11690 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ) |
| 17 | 9 | renegcld 11690 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → -𝑦 ∈ ℝ) |
| 18 | | maxlt 13235 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ -𝐵
∈ ℝ ∧ -𝑦
∈ ℝ) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ (0 < -𝑦 ∧ -𝐵 < -𝑦))) |
| 19 | 15, 16, 17, 18 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ (0 < -𝑦 ∧ -𝐵 < -𝑦))) |
| 20 | 12, 14, 19 | 3bitr4rd 312 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ 𝑦 < 𝐵)) |
| 21 | 1 | renegcld 11690 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ) |
| 22 | | ifcl 4571 |
. . . . . . . . . . . . . 14
⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
| 23 | 21, 4, 22 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
| 24 | 23 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
| 25 | 24 | biantrurd 532 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦))) |
| 26 | 13 | biantrurd 532 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 𝐵 ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
| 27 | 20, 25, 26 | 3bitr3d 309 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
| 28 | 17 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → -𝑦 ∈ ℝ*) |
| 29 | | elioomnf 13484 |
. . . . . . . . . . 11
⊢ (-𝑦 ∈ ℝ*
→ (if(0 ≤ -𝐵,
-𝐵, 0) ∈
(-∞(,)-𝑦) ↔
(if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0
≤ -𝐵, -𝐵, 0) < -𝑦))) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦))) |
| 31 | 9 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
| 32 | | elioopnf 13483 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (𝐵 ∈ (𝑦(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (𝑦(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
| 34 | 27, 30, 33 | 3bitr4d 311 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
| 35 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 36 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) |
| 37 | 36 | fvmpt2 7027 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) = if(0 ≤ -𝐵, -𝐵, 0)) |
| 38 | 35, 23, 37 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) = if(0 ≤ -𝐵, -𝐵, 0)) |
| 39 | 38 | eleq1d 2826 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦))) |
| 40 | 39 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦))) |
| 41 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 42 | 41 | fvmpt2 7027 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 43 | 35, 1, 42 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 44 | 43 | eleq1d 2826 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
| 45 | 44 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
| 46 | 34, 40, 45 | 3bitr4d 311 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞))) |
| 47 | 46 | pm5.32da 579 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → ((𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
| 48 | 23 | fmpttd 7135 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℝ) |
| 49 | | ffn 6736 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℝ → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) Fn 𝐴) |
| 50 | | elpreima 7078 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦)))) |
| 51 | 48, 49, 50 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦)))) |
| 52 | 51 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦)))) |
| 53 | | ffn 6736 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
| 54 | | elpreima 7078 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
| 55 | 2, 53, 54 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
| 56 | 55 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
| 57 | 47, 52, 56 | 3bitr4d 311 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
| 58 | 57 | alrimiv 1927 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
| 59 | | nfmpt1 5250 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) |
| 60 | 59 | nfcnv 5889 |
. . . . . . 7
⊢
Ⅎ𝑥◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) |
| 61 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥(-∞(,)-𝑦) |
| 62 | 60, 61 | nfima 6086 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) |
| 63 | | nfmpt1 5250 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 64 | 63 | nfcnv 5889 |
. . . . . . 7
⊢
Ⅎ𝑥◡(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 65 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑦(,)+∞) |
| 66 | 64, 65 | nfima 6086 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) |
| 67 | 62, 66 | cleqf 2934 |
. . . . 5
⊢ ((◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
| 68 | 58, 67 | sylibr 234 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞))) |
| 69 | | mbfposr.3 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn) |
| 70 | | mbfima 25665 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ∈ dom
vol) |
| 71 | 69, 48, 70 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ∈ dom
vol) |
| 72 | 71 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ∈ dom
vol) |
| 73 | 68, 72 | eqeltrrd 2842 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ∈ dom
vol) |
| 74 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝑦) |
| 75 | | 0red 11264 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
| 76 | 1 | ad4ant14 752 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| 77 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
| 78 | | maxle 13233 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ ∧ 𝑦
∈ ℝ) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ (0 ≤ 𝑦 ∧ 𝐵 ≤ 𝑦))) |
| 79 | 75, 76, 77, 78 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ (0 ≤ 𝑦 ∧ 𝐵 ≤ 𝑦))) |
| 80 | 74, 79 | mpbirand 707 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
| 81 | 80 | notbid 318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (¬ if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ ¬ 𝐵 ≤ 𝑦)) |
| 82 | 76, 4, 5 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
| 83 | 77, 82 | ltnled 11408 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < if(0 ≤ 𝐵, 𝐵, 0) ↔ ¬ if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦)) |
| 84 | 77, 76 | ltnled 11408 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 𝐵 ↔ ¬ 𝐵 ≤ 𝑦)) |
| 85 | 81, 83, 84 | 3bitr4d 311 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < if(0 ≤ 𝐵, 𝐵, 0) ↔ 𝑦 < 𝐵)) |
| 86 | 82 | biantrurd 532 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < if(0 ≤ 𝐵, 𝐵, 0) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0)))) |
| 87 | 76 | biantrurd 532 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 𝐵 ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
| 88 | 85, 86, 87 | 3bitr3d 309 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0)) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
| 89 | 77 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
| 90 | | elioopnf 13483 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0)))) |
| 91 | 89, 90 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0)))) |
| 92 | 89, 32 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (𝑦(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
| 93 | 88, 91, 92 | 3bitr4d 311 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
| 94 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) |
| 95 | 94 | fvmpt2 7027 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) = if(0 ≤ 𝐵, 𝐵, 0)) |
| 96 | 35, 6, 95 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) = if(0 ≤ 𝐵, 𝐵, 0)) |
| 97 | 96 | eleq1d 2826 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞))) |
| 98 | 97 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞))) |
| 99 | 44 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
| 100 | 93, 98, 99 | 3bitr4d 311 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞))) |
| 101 | 100 | pm5.32da 579 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → ((𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
| 102 | 6 | fmpttd 7135 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ) |
| 103 | | ffn 6736 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) Fn 𝐴) |
| 104 | | elpreima 7078 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞)))) |
| 105 | 102, 103,
104 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞)))) |
| 106 | 105 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞)))) |
| 107 | 55 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
| 108 | 101, 106,
107 | 3bitr4d 311 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
| 109 | 108 | alrimiv 1927 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
| 110 | | nfmpt1 5250 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) |
| 111 | 110 | nfcnv 5889 |
. . . . . . 7
⊢
Ⅎ𝑥◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) |
| 112 | 111, 65 | nfima 6086 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) |
| 113 | 112, 66 | cleqf 2934 |
. . . . 5
⊢ ((◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
| 114 | 109, 113 | sylibr 234 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞))) |
| 115 | | mbfima 25665 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ∈ dom
vol) |
| 116 | 3, 102, 115 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ∈ dom
vol) |
| 117 | 116 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ∈ dom
vol) |
| 118 | 114, 117 | eqeltrrd 2842 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ∈ dom
vol) |
| 119 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
| 120 | | 0red 11264 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ∈
ℝ) |
| 121 | 73, 118, 119, 120 | ltlecasei 11369 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ∈ dom
vol) |
| 122 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 0 < 𝑦) |
| 123 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
| 124 | 1 | ad4ant14 752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| 125 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
| 126 | | maxlt 13235 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ ∧ 𝑦
∈ ℝ) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ (0 < 𝑦 ∧ 𝐵 < 𝑦))) |
| 127 | 123, 124,
125, 126 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ (0 < 𝑦 ∧ 𝐵 < 𝑦))) |
| 128 | 122, 127 | mpbirand 707 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ 𝐵 < 𝑦)) |
| 129 | 6 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
| 130 | 129 | biantrurd 532 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦))) |
| 131 | 124 | biantrurd 532 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝐵 < 𝑦 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
| 132 | 128, 130,
131 | 3bitr3d 309 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
| 133 | 125 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
| 134 | | elioomnf 13484 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦))) |
| 135 | 133, 134 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦))) |
| 136 | | elioomnf 13484 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (𝐵 ∈
(-∞(,)𝑦) ↔
(𝐵 ∈ ℝ ∧
𝐵 < 𝑦))) |
| 137 | 133, 136 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (-∞(,)𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
| 138 | 132, 135,
137 | 3bitr4d 311 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
| 139 | 96 | eleq1d 2826 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦))) |
| 140 | 139 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦))) |
| 141 | 43 | eleq1d 2826 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
| 142 | 141 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
| 143 | 138, 140,
142 | 3bitr4d 311 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦))) |
| 144 | 143 | pm5.32da 579 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → ((𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
| 145 | | elpreima 7078 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦)))) |
| 146 | 102, 103,
145 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦)))) |
| 147 | 146 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦)))) |
| 148 | | elpreima 7078 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
| 149 | 2, 53, 148 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
| 150 | 149 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
| 151 | 144, 147,
150 | 3bitr4d 311 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
| 152 | 151 | alrimiv 1927 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
| 153 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥(-∞(,)𝑦) |
| 154 | 111, 153 | nfima 6086 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) |
| 155 | 64, 153 | nfima 6086 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) |
| 156 | 154, 155 | cleqf 2934 |
. . . . 5
⊢ ((◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
| 157 | 152, 156 | sylibr 234 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦))) |
| 158 | | mbfima 25665 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ∈ dom vol) |
| 159 | 3, 102, 158 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ∈ dom vol) |
| 160 | 159 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ∈ dom vol) |
| 161 | 157, 160 | eqeltrrd 2842 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ∈ dom vol) |
| 162 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ≤ 0) |
| 163 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
| 164 | 163 | le0neg1d 11834 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 ≤ 0 ↔ 0 ≤ -𝑦)) |
| 165 | 162, 164 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 0 ≤ -𝑦) |
| 166 | 165 | biantrurd 532 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (-𝐵 ≤ -𝑦 ↔ (0 ≤ -𝑦 ∧ -𝐵 ≤ -𝑦))) |
| 167 | 1 | ad4ant14 752 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| 168 | 163, 167 | lenegd 11842 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 ≤ 𝐵 ↔ -𝐵 ≤ -𝑦)) |
| 169 | | 0red 11264 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
| 170 | 167 | renegcld 11690 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ) |
| 171 | 163 | renegcld 11690 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → -𝑦 ∈ ℝ) |
| 172 | | maxle 13233 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ -𝐵
∈ ℝ ∧ -𝑦
∈ ℝ) → (if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ (0 ≤ -𝑦 ∧ -𝐵 ≤ -𝑦))) |
| 173 | 169, 170,
171, 172 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ (0 ≤ -𝑦 ∧ -𝐵 ≤ -𝑦))) |
| 174 | 166, 168,
173 | 3bitr4rd 312 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ 𝑦 ≤ 𝐵)) |
| 175 | 174 | notbid 318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (¬ if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ ¬ 𝑦 ≤ 𝐵)) |
| 176 | 23 | ad4ant14 752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
| 177 | 171, 176 | ltnled 11408 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (-𝑦 < if(0 ≤ -𝐵, -𝐵, 0) ↔ ¬ if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦)) |
| 178 | 167, 163 | ltnled 11408 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝐵 < 𝑦 ↔ ¬ 𝑦 ≤ 𝐵)) |
| 179 | 175, 177,
178 | 3bitr4d 311 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (-𝑦 < if(0 ≤ -𝐵, -𝐵, 0) ↔ 𝐵 < 𝑦)) |
| 180 | 176 | biantrurd 532 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (-𝑦 < if(0 ≤ -𝐵, -𝐵, 0) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0)))) |
| 181 | 167 | biantrurd 532 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝐵 < 𝑦 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
| 182 | 179, 180,
181 | 3bitr3d 309 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0)) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
| 183 | 171 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → -𝑦 ∈ ℝ*) |
| 184 | | elioopnf 13483 |
. . . . . . . . . . 11
⊢ (-𝑦 ∈ ℝ*
→ (if(0 ≤ -𝐵,
-𝐵, 0) ∈ (-𝑦(,)+∞) ↔ (if(0 ≤
-𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0)))) |
| 185 | 183, 184 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0)))) |
| 186 | 163 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
| 187 | 186, 136 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (-∞(,)𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
| 188 | 182, 185,
187 | 3bitr4d 311 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
| 189 | 38 | eleq1d 2826 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞))) |
| 190 | 189 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞))) |
| 191 | 141 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
| 192 | 188, 190,
191 | 3bitr4d 311 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦))) |
| 193 | 192 | pm5.32da 579 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → ((𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
| 194 | | elpreima 7078 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞)))) |
| 195 | 48, 49, 194 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞)))) |
| 196 | 195 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞)))) |
| 197 | 149 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
| 198 | 193, 196,
197 | 3bitr4d 311 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
| 199 | 198 | alrimiv 1927 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
| 200 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥(-𝑦(,)+∞) |
| 201 | 60, 200 | nfima 6086 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) |
| 202 | 201, 155 | cleqf 2934 |
. . . . 5
⊢ ((◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
| 203 | 199, 202 | sylibr 234 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦))) |
| 204 | | mbfima 25665 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ∈ dom
vol) |
| 205 | 69, 48, 204 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ∈ dom
vol) |
| 206 | 205 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ∈ dom
vol) |
| 207 | 203, 206 | eqeltrrd 2842 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ∈ dom vol) |
| 208 | 161, 207,
120, 119 | ltlecasei 11369 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ∈ dom vol) |
| 209 | 2, 7, 121, 208 | ismbf2d 25675 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |