MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfposr Structured version   Visualization version   GIF version

Theorem mbfposr 25687
Description: Converse to mbfpos 25686. (Contributed by Mario Carneiro, 11-Aug-2014.)
Hypotheses
Ref Expression
mbfpos.1 ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)
mbfposr.2 (𝜑 → (𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
mbfposr.3 (𝜑 → (𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn)
Assertion
Ref Expression
mbfposr (𝜑 → (𝑥𝐴𝐵) ∈ MblFn)
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem mbfposr
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 mbfpos.1 . . 3 ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)
21fmpttd 7135 . 2 (𝜑 → (𝑥𝐴𝐵):𝐴⟶ℝ)
3 mbfposr.2 . . 3 (𝜑 → (𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
4 0re 11263 . . . 4 0 ∈ ℝ
5 ifcl 4571 . . . 4 ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
61, 4, 5sylancl 586 . . 3 ((𝜑𝑥𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
73, 6mbfdm2 25672 . 2 (𝜑𝐴 ∈ dom vol)
8 simplr 769 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → 𝑦 < 0)
9 simpllr 776 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ)
109lt0neg1d 11832 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (𝑦 < 0 ↔ 0 < -𝑦))
118, 10mpbid 232 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → 0 < -𝑦)
1211biantrurd 532 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (-𝐵 < -𝑦 ↔ (0 < -𝑦 ∧ -𝐵 < -𝑦)))
131ad4ant14 752 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → 𝐵 ∈ ℝ)
149, 13ltnegd 11841 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (𝑦 < 𝐵 ↔ -𝐵 < -𝑦))
15 0red 11264 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → 0 ∈ ℝ)
1613renegcld 11690 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → -𝐵 ∈ ℝ)
179renegcld 11690 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → -𝑦 ∈ ℝ)
18 maxlt 13235 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ -𝐵 ∈ ℝ ∧ -𝑦 ∈ ℝ) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ (0 < -𝑦 ∧ -𝐵 < -𝑦)))
1915, 16, 17, 18syl3anc 1373 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ (0 < -𝑦 ∧ -𝐵 < -𝑦)))
2012, 14, 193bitr4rd 312 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦𝑦 < 𝐵))
211renegcld 11690 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → -𝐵 ∈ ℝ)
22 ifcl 4571 . . . . . . . . . . . . . 14 ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
2321, 4, 22sylancl 586 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
2423ad4ant14 752 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
2524biantrurd 532 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) < -𝑦 ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦)))
2613biantrurd 532 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (𝑦 < 𝐵 ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵)))
2720, 25, 263bitr3d 309 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → ((if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵)))
2817rexrd 11311 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → -𝑦 ∈ ℝ*)
29 elioomnf 13484 . . . . . . . . . . 11 (-𝑦 ∈ ℝ* → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦)))
3028, 29syl 17 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) < -𝑦)))
319rexrd 11311 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ*)
32 elioopnf 13483 . . . . . . . . . . 11 (𝑦 ∈ ℝ* → (𝐵 ∈ (𝑦(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵)))
3331, 32syl 17 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (𝐵 ∈ (𝑦(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵)))
3427, 30, 333bitr4d 311 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦) ↔ 𝐵 ∈ (𝑦(,)+∞)))
35 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑥𝐴)
36 eqid 2737 . . . . . . . . . . . . 13 (𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) = (𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))
3736fvmpt2 7027 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) → ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) = if(0 ≤ -𝐵, -𝐵, 0))
3835, 23, 37syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) = if(0 ≤ -𝐵, -𝐵, 0))
3938eleq1d 2826 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦)))
4039ad4ant14 752 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-∞(,)-𝑦)))
41 eqid 2737 . . . . . . . . . . . . 13 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
4241fvmpt2 7027 . . . . . . . . . . . 12 ((𝑥𝐴𝐵 ∈ ℝ) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
4335, 1, 42syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
4443eleq1d 2826 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞)))
4544ad4ant14 752 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞)))
4634, 40, 453bitr4d 311 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) ∧ 𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦) ↔ ((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞)))
4746pm5.32da 579 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) → ((𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞))))
4823fmpttd 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))‘𝑥) ∈ (-∞(,)-𝑦))))
5148, 49, 503syl 18 . . . . . . . 8 (𝜑 → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦))))
5251ad2antrr 726 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-∞(,)-𝑦))))
53 ffn 6736 . . . . . . . . 9 ((𝑥𝐴𝐵):𝐴⟶ℝ → (𝑥𝐴𝐵) Fn 𝐴)
54 elpreima 7078 . . . . . . . . 9 ((𝑥𝐴𝐵) Fn 𝐴 → (𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞))))
552, 53, 543syl 18 . . . . . . . 8 (𝜑 → (𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞))))
5655ad2antrr 726 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞))))
5747, 52, 563bitr4d 311 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞))))
5857alrimiv 1927 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) → ∀𝑥(𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞))))
59 nfmpt1 5250 . . . . . . . 8 𝑥(𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))
6059nfcnv 5889 . . . . . . 7 𝑥(𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))
61 nfcv 2905 . . . . . . 7 𝑥(-∞(,)-𝑦)
6260, 61nfima 6086 . . . . . 6 𝑥((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦))
63 nfmpt1 5250 . . . . . . . 8 𝑥(𝑥𝐴𝐵)
6463nfcnv 5889 . . . . . . 7 𝑥(𝑥𝐴𝐵)
65 nfcv 2905 . . . . . . 7 𝑥(𝑦(,)+∞)
6664, 65nfima 6086 . . . . . 6 𝑥((𝑥𝐴𝐵) “ (𝑦(,)+∞))
6762, 66cleqf 2934 . . . . 5 (((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) = ((𝑥𝐴𝐵) “ (𝑦(,)+∞)) ↔ ∀𝑥(𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞))))
6858, 67sylibr 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)
7169, 48, 70syl2anc 584 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ∈ dom vol)
7271ad2antrr 726 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) → ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-∞(,)-𝑦)) ∈ dom vol)
7368, 72eqeltrrd 2842 . . 3 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 < 0) → ((𝑥𝐴𝐵) “ (𝑦(,)+∞)) ∈ dom vol)
74 simplr 769 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → 0 ≤ 𝑦)
75 0red 11264 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → 0 ∈ ℝ)
761ad4ant14 752 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → 𝐵 ∈ ℝ)
77 simpllr 776 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ)
78 maxle 13233 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ (0 ≤ 𝑦𝐵𝑦)))
7975, 76, 77, 78syl3anc 1373 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ (0 ≤ 𝑦𝐵𝑦)))
8074, 79mpbirand 707 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦𝐵𝑦))
8180notbid 318 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (¬ if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦 ↔ ¬ 𝐵𝑦))
8276, 4, 5sylancl 586 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
8377, 82ltnled 11408 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (𝑦 < if(0 ≤ 𝐵, 𝐵, 0) ↔ ¬ if(0 ≤ 𝐵, 𝐵, 0) ≤ 𝑦))
8477, 76ltnled 11408 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (𝑦 < 𝐵 ↔ ¬ 𝐵𝑦))
8581, 83, 843bitr4d 311 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (𝑦 < if(0 ≤ 𝐵, 𝐵, 0) ↔ 𝑦 < 𝐵))
8682biantrurd 532 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (𝑦 < if(0 ≤ 𝐵, 𝐵, 0) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0))))
8776biantrurd 532 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (𝑦 < 𝐵 ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵)))
8885, 86, 873bitr3d 309 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → ((if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0)) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵)))
8977rexrd 11311 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ*)
90 elioopnf 13483 . . . . . . . . . . 11 (𝑦 ∈ ℝ* → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0))))
9189, 90syl 17 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ 𝑦 < if(0 ≤ 𝐵, 𝐵, 0))))
9289, 32syl 17 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (𝐵 ∈ (𝑦(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑦 < 𝐵)))
9388, 91, 923bitr4d 311 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞)))
94 eqid 2737 . . . . . . . . . . . . 13 (𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))
9594fvmpt2 7027 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) = if(0 ≤ 𝐵, 𝐵, 0))
9635, 6, 95syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) = if(0 ≤ 𝐵, 𝐵, 0))
9796eleq1d 2826 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞)))
9897ad4ant14 752 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (𝑦(,)+∞)))
9944ad4ant14 752 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝐵 ∈ (𝑦(,)+∞)))
10093, 98, 993bitr4d 311 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) ∧ 𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞) ↔ ((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞)))
101100pm5.32da 579 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → ((𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞))))
1026fmpttd 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))‘𝑥) ∈ (𝑦(,)+∞))))
105102, 103, 1043syl 18 . . . . . . . 8 (𝜑 → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞))))
106105ad2antrr 726 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (𝑦(,)+∞))))
10755ad2antrr 726 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (𝑦(,)+∞))))
108101, 106, 1073bitr4d 311 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞))))
109108alrimiv 1927 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → ∀𝑥(𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞))))
110 nfmpt1 5250 . . . . . . . 8 𝑥(𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))
111110nfcnv 5889 . . . . . . 7 𝑥(𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))
112111, 65nfima 6086 . . . . . 6 𝑥((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞))
113112, 66cleqf 2934 . . . . 5 (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) = ((𝑥𝐴𝐵) “ (𝑦(,)+∞)) ↔ ∀𝑥(𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (𝑦(,)+∞))))
114109, 113sylibr 234 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) = ((𝑥𝐴𝐵) “ (𝑦(,)+∞)))
115 mbfima 25665 . . . . . 6 (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ (𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ) → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ∈ dom vol)
1163, 102, 115syl2anc 584 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ∈ dom vol)
117116ad2antrr 726 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (𝑦(,)+∞)) ∈ dom vol)
118114, 117eqeltrrd 2842 . . 3 (((𝜑𝑦 ∈ ℝ) ∧ 0 ≤ 𝑦) → ((𝑥𝐴𝐵) “ (𝑦(,)+∞)) ∈ dom vol)
119 simpr 484 . . 3 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
120 0red 11264 . . 3 ((𝜑𝑦 ∈ ℝ) → 0 ∈ ℝ)
12173, 118, 119, 120ltlecasei 11369 . 2 ((𝜑𝑦 ∈ ℝ) → ((𝑥𝐴𝐵) “ (𝑦(,)+∞)) ∈ dom vol)
122 simplr 769 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → 0 < 𝑦)
123 0red 11264 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → 0 ∈ ℝ)
1241ad4ant14 752 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → 𝐵 ∈ ℝ)
125 simpllr 776 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ)
126 maxlt 13235 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ (0 < 𝑦𝐵 < 𝑦)))
127123, 124, 125, 126syl3anc 1373 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ (0 < 𝑦𝐵 < 𝑦)))
128122, 127mpbirand 707 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦𝐵 < 𝑦))
1296ad4ant14 752 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
130129biantrurd 532 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) < 𝑦 ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦)))
131124biantrurd 532 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (𝐵 < 𝑦 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦)))
132128, 130, 1313bitr3d 309 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → ((if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦)))
133125rexrd 11311 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ*)
134 elioomnf 13484 . . . . . . . . . . 11 (𝑦 ∈ ℝ* → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦)))
135133, 134syl 17 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦) ↔ (if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ ∧ if(0 ≤ 𝐵, 𝐵, 0) < 𝑦)))
136 elioomnf 13484 . . . . . . . . . . 11 (𝑦 ∈ ℝ* → (𝐵 ∈ (-∞(,)𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦)))
137133, 136syl 17 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (𝐵 ∈ (-∞(,)𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦)))
138132, 135, 1373bitr4d 311 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦)))
13996eleq1d 2826 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦)))
140139ad4ant14 752 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦) ↔ if(0 ≤ 𝐵, 𝐵, 0) ∈ (-∞(,)𝑦)))
14143eleq1d 2826 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦)))
142141ad4ant14 752 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦)))
143138, 140, 1423bitr4d 311 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) ∧ 𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦) ↔ ((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦)))
144143pm5.32da 579 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) → ((𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦))))
145 elpreima 7078 . . . . . . . . 9 ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) Fn 𝐴 → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦))))
146102, 103, 1453syl 18 . . . . . . . 8 (𝜑 → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦))))
147146ad2antrr 726 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))‘𝑥) ∈ (-∞(,)𝑦))))
148 elpreima 7078 . . . . . . . . 9 ((𝑥𝐴𝐵) Fn 𝐴 → (𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦))))
1492, 53, 1483syl 18 . . . . . . . 8 (𝜑 → (𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦))))
150149ad2antrr 726 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦))))
151144, 147, 1503bitr4d 311 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦))))
152151alrimiv 1927 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) → ∀𝑥(𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦))))
153 nfcv 2905 . . . . . . 7 𝑥(-∞(,)𝑦)
154111, 153nfima 6086 . . . . . 6 𝑥((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦))
15564, 153nfima 6086 . . . . . 6 𝑥((𝑥𝐴𝐵) “ (-∞(,)𝑦))
156154, 155cleqf 2934 . . . . 5 (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) = ((𝑥𝐴𝐵) “ (-∞(,)𝑦)) ↔ ∀𝑥(𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦))))
157152, 156sylibr 234 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) = ((𝑥𝐴𝐵) “ (-∞(,)𝑦)))
158 mbfima 25665 . . . . . 6 (((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ (𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℝ) → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ∈ dom vol)
1593, 102, 158syl2anc 584 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ∈ dom vol)
160159ad2antrr 726 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) → ((𝑥𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) “ (-∞(,)𝑦)) ∈ dom vol)
161157, 160eqeltrrd 2842 . . 3 (((𝜑𝑦 ∈ ℝ) ∧ 0 < 𝑦) → ((𝑥𝐴𝐵) “ (-∞(,)𝑦)) ∈ dom vol)
162 simplr 769 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → 𝑦 ≤ 0)
163 simpllr 776 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ)
164163le0neg1d 11834 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (𝑦 ≤ 0 ↔ 0 ≤ -𝑦))
165162, 164mpbid 232 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → 0 ≤ -𝑦)
166165biantrurd 532 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (-𝐵 ≤ -𝑦 ↔ (0 ≤ -𝑦 ∧ -𝐵 ≤ -𝑦)))
1671ad4ant14 752 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → 𝐵 ∈ ℝ)
168163, 167lenegd 11842 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (𝑦𝐵 ↔ -𝐵 ≤ -𝑦))
169 0red 11264 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → 0 ∈ ℝ)
170167renegcld 11690 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → -𝐵 ∈ ℝ)
171163renegcld 11690 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → -𝑦 ∈ ℝ)
172 maxle 13233 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ -𝐵 ∈ ℝ ∧ -𝑦 ∈ ℝ) → (if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ (0 ≤ -𝑦 ∧ -𝐵 ≤ -𝑦)))
173169, 170, 171, 172syl3anc 1373 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ (0 ≤ -𝑦 ∧ -𝐵 ≤ -𝑦)))
174166, 168, 1733bitr4rd 312 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦𝑦𝐵))
175174notbid 318 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (¬ if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦 ↔ ¬ 𝑦𝐵))
17623ad4ant14 752 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
177171, 176ltnled 11408 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (-𝑦 < if(0 ≤ -𝐵, -𝐵, 0) ↔ ¬ if(0 ≤ -𝐵, -𝐵, 0) ≤ -𝑦))
178167, 163ltnled 11408 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (𝐵 < 𝑦 ↔ ¬ 𝑦𝐵))
179175, 177, 1783bitr4d 311 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (-𝑦 < if(0 ≤ -𝐵, -𝐵, 0) ↔ 𝐵 < 𝑦))
180176biantrurd 532 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (-𝑦 < if(0 ≤ -𝐵, -𝐵, 0) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0))))
181167biantrurd 532 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (𝐵 < 𝑦 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦)))
182179, 180, 1813bitr3d 309 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → ((if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0)) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦)))
183171rexrd 11311 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → -𝑦 ∈ ℝ*)
184 elioopnf 13483 . . . . . . . . . . 11 (-𝑦 ∈ ℝ* → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0))))
185183, 184syl 17 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞) ↔ (if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ ∧ -𝑦 < if(0 ≤ -𝐵, -𝐵, 0))))
186163rexrd 11311 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ*)
187186, 136syl 17 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (𝐵 ∈ (-∞(,)𝑦) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝑦)))
188182, 185, 1873bitr4d 311 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞) ↔ 𝐵 ∈ (-∞(,)𝑦)))
18938eleq1d 2826 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞)))
190189ad4ant14 752 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞) ↔ if(0 ≤ -𝐵, -𝐵, 0) ∈ (-𝑦(,)+∞)))
191141ad4ant14 752 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦) ↔ 𝐵 ∈ (-∞(,)𝑦)))
192188, 190, 1913bitr4d 311 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) ∧ 𝑥𝐴) → (((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞) ↔ ((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦)))
193192pm5.32da 579 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → ((𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦))))
194 elpreima 7078 . . . . . . . . 9 ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) Fn 𝐴 → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞))))
19548, 49, 1943syl 18 . . . . . . . 8 (𝜑 → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞))))
196195ad2antrr 726 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))‘𝑥) ∈ (-𝑦(,)+∞))))
197149ad2antrr 726 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦)) ↔ (𝑥𝐴 ∧ ((𝑥𝐴𝐵)‘𝑥) ∈ (-∞(,)𝑦))))
198193, 196, 1973bitr4d 311 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → (𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦))))
199198alrimiv 1927 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → ∀𝑥(𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦))))
200 nfcv 2905 . . . . . . 7 𝑥(-𝑦(,)+∞)
20160, 200nfima 6086 . . . . . 6 𝑥((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞))
202201, 155cleqf 2934 . . . . 5 (((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) = ((𝑥𝐴𝐵) “ (-∞(,)𝑦)) ↔ ∀𝑥(𝑥 ∈ ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ↔ 𝑥 ∈ ((𝑥𝐴𝐵) “ (-∞(,)𝑦))))
203199, 202sylibr 234 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) = ((𝑥𝐴𝐵) “ (-∞(,)𝑦)))
204 mbfima 25665 . . . . . 6 (((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn ∧ (𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℝ) → ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ∈ dom vol)
20569, 48, 204syl2anc 584 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ∈ dom vol)
206205ad2antrr 726 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → ((𝑥𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) “ (-𝑦(,)+∞)) ∈ dom vol)
207203, 206eqeltrrd 2842 . . 3 (((𝜑𝑦 ∈ ℝ) ∧ 𝑦 ≤ 0) → ((𝑥𝐴𝐵) “ (-∞(,)𝑦)) ∈ dom vol)
208161, 207, 120, 119ltlecasei 11369 . 2 ((𝜑𝑦 ∈ ℝ) → ((𝑥𝐴𝐵) “ (-∞(,)𝑦)) ∈ dom vol)
2092, 7, 121, 208ismbf2d 25675 1 (𝜑 → (𝑥𝐴𝐵) ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1538   = wceq 1540  wcel 2108  ifcif 4525   class class class wbr 5143  cmpt 5225  ccnv 5684  dom cdm 5685  cima 5688   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  cr 11154  0cc0 11155  +∞cpnf 11292  -∞cmnf 11293  *cxr 11294   < clt 11295  cle 11296  -cneg 11493  (,)cioo 13387  volcvol 25498  MblFncmbf 25649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-xadd 13155  df-ioo 13391  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-xmet 21357  df-met 21358  df-ovol 25499  df-vol 25500  df-mbf 25654
This theorem is referenced by:  mbfposb  25688
  Copyright terms: Public domain W3C validator