Metamath Proof Explorer

Theorem mbfposr

Description: Converse to mbfpos . (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses mbfpos.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
mbfposr.2 ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn
mbfposr.3 ⊢ φ → x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn
Assertion mbfposr ⊢ φ → x ∈ A ⟼ B ∈ MblFn

Proof

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