Step | Hyp | Ref
| Expression |
1 | | mbfpos.1 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
2 | | eqid 2610 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
3 | 1, 2 | fmptd 6292 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) |
4 | | mbfposr.2 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) |
5 | | 0re 9919 |
. . . 4
⊢ 0 ∈
ℝ |
6 | | ifcl 4080 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
7 | 1, 5, 6 | sylancl 693 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
8 | 4, 7 | mbfdm2 23211 |
. 2
⊢ (𝜑 → 𝐴 ∈ dom vol) |
9 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 < 0) |
10 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
11 | 10 | lt0neg1d 10476 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 0 ↔ 0 < -𝑦)) |
12 | 9, 11 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 0 < -𝑦) |
13 | 12 | biantrurd 528 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (-𝐵 < -𝑦 ↔ (0 < -𝑦 ∧ -𝐵 < -𝑦))) |
14 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → 𝜑) |
15 | 14, 1 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
16 | 10, 15 | ltnegd 10484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 𝐵 ↔ -𝐵 < -𝑦)) |
17 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
18 | 15 | renegcld 10336 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ) |
19 | 10 | renegcld 10336 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → -𝑦 ∈ ℝ) |
20 | | maxlt 11898 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ -𝐵
∈ ℝ ∧ -𝑦
∈ ℝ) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ (0 < -𝑦 ∧ -𝐵 < -𝑦))) |
21 | 17, 18, 19, 20 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ (0 < -𝑦 ∧ -𝐵 < -𝑦))) |
22 | 13, 16, 21 | 3bitr4rd 300 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ 𝑦 < 𝐵)) |
23 | 1 | renegcld 10336 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ) |
24 | | ifcl 4080 |
. . . . . . . . . . . . . 14
⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
25 | 23, 5, 24 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
26 | 14, 25 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
27 | 26 | biantrurd 528 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦))) |
28 | 15 | biantrurd 528 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 𝐵 ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
29 | 22, 27, 28 | 3bitr3d 297 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
30 | 19 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → -𝑦 ∈ ℝ*) |
31 | | elioomnf 12139 |
. . . . . . . . . . 11
⊢ (-𝑦 ∈ ℝ*
→ (if(0 ≤ -𝐵,
-𝐵, 0) ∈
(-∞(,)-𝑦) ↔
(if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0
≤ -𝐵, -𝐵, 0) < -𝑦))) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦))) |
33 | 10 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
34 | | elioopnf 12138 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (𝐵 ∈ (𝑦(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (𝑦(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
36 | 29, 32, 35 | 3bitr4d 299 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
37 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
38 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) |
39 | 38 | fvmpt2 6200 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) = if(0 ≤ -𝐵, -𝐵, 0)) |
40 | 37, 25, 39 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) = if(0 ≤ -𝐵, -𝐵, 0)) |
41 | 40 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦))) |
42 | 14, 41 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦))) |
43 | 2 | fvmpt2 6200 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
44 | 37, 1, 43 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
45 | 44 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
46 | 14, 45 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
47 | 36, 42, 46 | 3bitr4d 299 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞))) |
48 | 47 | pm5.32da 671 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → ((𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
49 | 25, 38 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℝ) |
50 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℝ → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) Fn 𝐴) |
51 | | elpreima 6245 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦)))) |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦)))) |
53 | 52 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦)))) |
54 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
55 | | elpreima 6245 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
56 | 3, 54, 55 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
57 | 56 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
58 | 48, 53, 57 | 3bitr4d 299 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
59 | 58 | alrimiv 1842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
60 | | nfmpt1 4675 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) |
61 | 60 | nfcnv 5223 |
. . . . . . 7
⊢
Ⅎ𝑥◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) |
62 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥(-∞(,)-𝑦) |
63 | 61, 62 | nfima 5393 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) |
64 | | nfmpt1 4675 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
65 | 64 | nfcnv 5223 |
. . . . . . 7
⊢
Ⅎ𝑥◡(𝑥 ∈ 𝐴 ↦ 𝐵) |
66 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑦(,)+∞) |
67 | 65, 66 | nfima 5393 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) |
68 | 63, 67 | cleqf 2776 |
. . . . 5
⊢ ((◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
69 | 59, 68 | sylibr 223 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞))) |
70 | | mbfposr.3 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn) |
71 | | mbfima 23205 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ∈ dom
vol) |
72 | 70, 49, 71 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ∈ dom
vol) |
73 | 72 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ∈ dom
vol) |
74 | 69, 73 | eqeltrrd 2689 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ∈ dom
vol) |
75 | | 0red 9920 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
76 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → 𝜑) |
77 | 76, 1 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
78 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
79 | | maxle 11896 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ ∧ 𝑦
∈ ℝ) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ (0 ≤ 𝑦 ∧ 𝐵 ≤ 𝑦))) |
80 | 75, 77, 78, 79 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ (0 ≤ 𝑦 ∧ 𝐵 ≤ 𝑦))) |
81 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝑦) |
82 | 81 | biantrurd 528 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 𝑦 ↔ (0 ≤ 𝑦 ∧ 𝐵 ≤ 𝑦))) |
83 | 80, 82 | bitr4d 270 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
84 | 83 | notbid 307 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (¬ if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ ¬ 𝐵 ≤ 𝑦)) |
85 | 77, 5, 6 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
86 | 78, 85 | ltnled 10063 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < if(0 ≤ 𝐵, 𝐵, 0) ↔ ¬ if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦)) |
87 | 78, 77 | ltnled 10063 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 𝐵 ↔ ¬ 𝐵 ≤ 𝑦)) |
88 | 84, 86, 87 | 3bitr4d 299 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < if(0 ≤ 𝐵, 𝐵, 0) ↔ 𝑦 < 𝐵)) |
89 | 85 | biantrurd 528 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < if(0 ≤ 𝐵, 𝐵, 0) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0)))) |
90 | 77 | biantrurd 528 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑦 < 𝐵 ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
91 | 88, 89, 90 | 3bitr3d 297 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0)) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
92 | 78 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
93 | | elioopnf 12138 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0)))) |
94 | 92, 93 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0)))) |
95 | 92, 34 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (𝑦(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵))) |
96 | 91, 94, 95 | 3bitr4d 299 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
97 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) |
98 | 97 | fvmpt2 6200 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) = if(0 ≤ 𝐵, 𝐵, 0)) |
99 | 37, 7, 98 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) = if(0 ≤ 𝐵, 𝐵, 0)) |
100 | 99 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞))) |
101 | 76, 100 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞))) |
102 | 76, 45 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞))) |
103 | 96, 101, 102 | 3bitr4d 299 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞))) |
104 | 103 | pm5.32da 671 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → ((𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
105 | 7, 97 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ) |
106 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) Fn 𝐴) |
107 | | elpreima 6245 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞)))) |
108 | 105, 106,
107 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞)))) |
109 | 108 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞)))) |
110 | 56 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑦(,)+∞)))) |
111 | 104, 109,
110 | 3bitr4d 299 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
112 | 111 | alrimiv 1842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
113 | | nfmpt1 4675 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) |
114 | 113 | nfcnv 5223 |
. . . . . . 7
⊢
Ⅎ𝑥◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) |
115 | 114, 66 | nfima 5393 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) |
116 | 115, 67 | cleqf 2776 |
. . . . 5
⊢ ((◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ↔ ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)))) |
117 | 112, 116 | sylibr 223 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞))) |
118 | | mbfima 23205 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ∈ dom
vol) |
119 | 4, 105, 118 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ∈ dom
vol) |
120 | 119 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ∈ dom
vol) |
121 | 117, 120 | eqeltrrd 2689 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ∈ dom
vol) |
122 | | simpr 476 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
123 | | 0red 9920 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ∈
ℝ) |
124 | 74, 121, 122, 123 | ltlecasei 10024 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑦(,)+∞)) ∈ dom
vol) |
125 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
126 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → 𝜑) |
127 | 126, 1 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
128 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
129 | | maxlt 11898 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ ∧ 𝑦
∈ ℝ) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ (0 < 𝑦 ∧ 𝐵 < 𝑦))) |
130 | 125, 127,
128, 129 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ (0 < 𝑦 ∧ 𝐵 < 𝑦))) |
131 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 0 < 𝑦) |
132 | 131 | biantrurd 528 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝐵 < 𝑦 ↔ (0 < 𝑦 ∧ 𝐵 < 𝑦))) |
133 | 130, 132 | bitr4d 270 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ 𝐵 < 𝑦)) |
134 | 126, 7 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
135 | 134 | biantrurd 528 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦))) |
136 | 127 | biantrurd 528 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝐵 < 𝑦 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
137 | 133, 135,
136 | 3bitr3d 297 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
138 | 128 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
139 | | elioomnf 12139 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦))) |
140 | 138, 139 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦))) |
141 | | elioomnf 12139 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (𝐵 ∈
(-∞(,)𝑦) ↔
(𝐵 ∈ ℝ ∧
𝐵 < 𝑦))) |
142 | 138, 141 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (-∞(,)𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
143 | 137, 140,
142 | 3bitr4d 299 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
144 | 99 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦))) |
145 | 126, 144 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦))) |
146 | 44 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
147 | 126, 146 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
148 | 143, 145,
147 | 3bitr4d 299 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦))) |
149 | 148 | pm5.32da 671 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → ((𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
150 | | elpreima 6245 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦)))) |
151 | 105, 106,
150 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦)))) |
152 | 151 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦)))) |
153 | | elpreima 6245 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
154 | 3, 54, 153 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
155 | 154 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
156 | 149, 152,
155 | 3bitr4d 299 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
157 | 156 | alrimiv 1842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
158 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥(-∞(,)𝑦) |
159 | 114, 158 | nfima 5393 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) |
160 | 65, 158 | nfima 5393 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) |
161 | 159, 160 | cleqf 2776 |
. . . . 5
⊢ ((◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
162 | 157, 161 | sylibr 223 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦))) |
163 | | mbfima 23205 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ∈ dom vol) |
164 | 4, 105, 163 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ∈ dom vol) |
165 | 164 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ∈ dom vol) |
166 | 162, 165 | eqeltrrd 2689 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ∈ dom vol) |
167 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ≤ 0) |
168 | | simpllr 795 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
169 | 168 | le0neg1d 10478 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 ≤ 0 ↔ 0 ≤ -𝑦)) |
170 | 167, 169 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 0 ≤ -𝑦) |
171 | 170 | biantrurd 528 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (-𝐵 ≤ -𝑦 ↔ (0 ≤ -𝑦 ∧ -𝐵 ≤ -𝑦))) |
172 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → 𝜑) |
173 | 172, 1 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
174 | 168, 173 | lenegd 10485 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝑦 ≤ 𝐵 ↔ -𝐵 ≤ -𝑦)) |
175 | | 0red 9920 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
176 | 173 | renegcld 10336 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ) |
177 | 168 | renegcld 10336 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → -𝑦 ∈ ℝ) |
178 | | maxle 11896 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ -𝐵
∈ ℝ ∧ -𝑦
∈ ℝ) → (if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ (0 ≤ -𝑦 ∧ -𝐵 ≤ -𝑦))) |
179 | 175, 176,
177, 178 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ (0 ≤ -𝑦 ∧ -𝐵 ≤ -𝑦))) |
180 | 171, 174,
179 | 3bitr4rd 300 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ 𝑦 ≤ 𝐵)) |
181 | 180 | notbid 307 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (¬ if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ ¬ 𝑦 ≤ 𝐵)) |
182 | 172, 25 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
183 | 177, 182 | ltnled 10063 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (-𝑦 < if(0 ≤ -𝐵, -𝐵, 0) ↔ ¬ if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦)) |
184 | 173, 168 | ltnled 10063 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝐵 < 𝑦 ↔ ¬ 𝑦 ≤ 𝐵)) |
185 | 181, 183,
184 | 3bitr4d 299 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (-𝑦 < if(0 ≤ -𝐵, -𝐵, 0) ↔ 𝐵 < 𝑦)) |
186 | 182 | biantrurd 528 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (-𝑦 < if(0 ≤ -𝐵, -𝐵, 0) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0)))) |
187 | 173 | biantrurd 528 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝐵 < 𝑦 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
188 | 185, 186,
187 | 3bitr3d 297 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0)) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
189 | 177 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → -𝑦 ∈ ℝ*) |
190 | | elioopnf 12138 |
. . . . . . . . . . 11
⊢ (-𝑦 ∈ ℝ*
→ (if(0 ≤ -𝐵,
-𝐵, 0) ∈ (-𝑦(,)+∞) ↔ (if(0 ≤
-𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0)))) |
191 | 189, 190 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0)))) |
192 | 168 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
193 | 192, 141 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (-∞(,)𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦))) |
194 | 188, 191,
193 | 3bitr4d 299 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
195 | 40 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞))) |
196 | 172, 195 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞))) |
197 | 172, 146 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦))) |
198 | 194, 196,
197 | 3bitr4d 299 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦))) |
199 | 198 | pm5.32da 671 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → ((𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
200 | | elpreima 6245 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) Fn 𝐴 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞)))) |
201 | 49, 50, 200 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞)))) |
202 | 201 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞)))) |
203 | 154 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (-∞(,)𝑦)))) |
204 | 199, 202,
203 | 3bitr4d 299 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
205 | 204 | alrimiv 1842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
206 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥(-𝑦(,)+∞) |
207 | 61, 206 | nfima 5393 |
. . . . . 6
⊢
Ⅎ𝑥(◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) |
208 | 207, 160 | cleqf 2776 |
. . . . 5
⊢ ((◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ↔ ∀𝑥(𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ 𝑥 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)))) |
209 | 205, 208 | sylibr 223 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦))) |
210 | | mbfima 23205 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ∈ dom
vol) |
211 | 70, 49, 210 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ∈ dom
vol) |
212 | 211 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (◡(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ∈ dom
vol) |
213 | 209, 212 | eqeltrrd 2689 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ∈ dom vol) |
214 | 166, 213,
123, 122 | ltlecasei 10024 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)𝑦)) ∈ dom vol) |
215 | 3, 8, 124, 214 | ismbf2d 23214 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |