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⟼if0≤BB0∈MblFn
mbfposr.3 ⊢φ→x∈A⟼if0≤−B−B0∈MblFn
Assertion mbfposr ⊢φ→x∈A⟼B∈MblFn

Proof

Step Hyp Ref Expression
1 mbfpos.1 ⊢φ∧x∈A→B∈ℝ
2 mbfposr.2 ⊢φ→x∈A⟼if0≤BB0∈MblFn
3 mbfposr.3 ⊢φ→x∈A⟼if0≤−B−B0∈MblFn
4 1 fmpttd ⊢φ→x∈A⟼B:A⟶ℝ
5 0re ⊢0∈ℝ
6 ifcl ⊢B∈ℝ∧0∈ℝ→if0≤BB0∈ℝ
7 1 5 6 sylancl ⊢φ∧x∈A→if0≤BB0∈ℝ
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∈ℝ→if0≤−B−B0<−y↔0<−y∧−B<−y
20 16 17 18 19 syl3anc ⊢φ∧y∈ℝ∧y<0∧x∈A→if0≤−B−B0<−y↔0<−y∧−B<−y
21 13 15 20 3bitr4rd ⊢φ∧y∈ℝ∧y<0∧x∈A→if0≤−B−B0<−y↔y<B
22 1 renegcld ⊢φ∧x∈A→−B∈ℝ
23 ifcl ⊢−B∈ℝ∧0∈ℝ→if0≤−B−B0∈ℝ
24 22 5 23 sylancl ⊢φ∧x∈A→if0≤−B−B0∈ℝ
25 24 ad4ant14 ⊢φ∧y∈ℝ∧y<0∧x∈A→if0≤−B−B0∈ℝ
26 25 biantrurd ⊢φ∧y∈ℝ∧y<0∧x∈A→if0≤−B−B0<−y↔if0≤−B−B0∈ℝ∧if0≤−B−B0<−y
27 14 biantrurd ⊢φ∧y∈ℝ∧y<0∧x∈A→y<B↔B∈ℝ∧y<B
28 21 26 27 3bitr3d ⊢φ∧y∈ℝ∧y<0∧x∈A→if0≤−B−B0∈ℝ∧if0≤−B−B0<−y↔B∈ℝ∧y<B
29 18 rexrd ⊢φ∧y∈ℝ∧y<0∧x∈A→−y∈ℝ*
30 elioomnf ⊢−y∈ℝ*→if0≤−B−B0∈−∞−y↔if0≤−B−B0∈ℝ∧if0≤−B−B0<−y
31 29 30 syl ⊢φ∧y∈ℝ∧y<0∧x∈A→if0≤−B−B0∈−∞−y↔if0≤−B−B0∈ℝ∧if0≤−B−B0<−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→if0≤−B−B0∈−∞−y↔B∈y+∞
36 simpr ⊢φ∧x∈A→x∈A
37 eqid ⊢x∈A⟼if0≤−B−B0=x∈A⟼if0≤−B−B0
38 37 fvmpt2 ⊢x∈A∧if0≤−B−B0∈ℝ→x∈A⟼if0≤−B−B0⁡x=if0≤−B−B0
39 36 24 38 syl2anc ⊢φ∧x∈A→x∈A⟼if0≤−B−B0⁡x=if0≤−B−B0
40 39 eleq1d ⊢φ∧x∈A→x∈A⟼if0≤−B−B0⁡x∈−∞−y↔if0≤−B−B0∈−∞−y
41 40 ad4ant14 ⊢φ∧y∈ℝ∧y<0∧x∈A→x∈A⟼if0≤−B−B0⁡x∈−∞−y↔if0≤−B−B0∈−∞−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⟼if0≤−B−B0⁡x∈−∞−y↔x∈A⟼B⁡x∈y+∞
48 47 pm5.32da ⊢φ∧y∈ℝ∧y<0→x∈A∧x∈A⟼if0≤−B−B0⁡x∈−∞−y↔x∈A∧x∈A⟼B⁡x∈y+∞
49 24 fmpttd ⊢φ→x∈A⟼if0≤−B−B0:A⟶ℝ
50 ffn ⊢x∈A⟼if0≤−B−B0:A⟶ℝ→x∈A⟼if0≤−B−B0FnA
51 elpreima ⊢x∈A⟼if0≤−B−B0FnA→x∈x∈A⟼if0≤−B−B0-1−∞−y↔x∈A∧x∈A⟼if0≤−B−B0⁡x∈−∞−y
52 49 50 51 3syl ⊢φ→x∈x∈A⟼if0≤−B−B0-1−∞−y↔x∈A∧x∈A⟼if0≤−B−B0⁡x∈−∞−y
53 52 ad2antrr ⊢φ∧y∈ℝ∧y<0→x∈x∈A⟼if0≤−B−B0-1−∞−y↔x∈A∧x∈A⟼if0≤−B−B0⁡x∈−∞−y
54 ffn ⊢x∈A⟼B:A⟶ℝ→x∈A⟼BFnA
55 elpreima ⊢x∈A⟼BFnA→x∈x∈A⟼B-1y+∞↔x∈A∧x∈A⟼B⁡x∈y+∞
56 4 54 55 3syl ⊢φ→x∈x∈A⟼B-1y+∞↔x∈A∧x∈A⟼B⁡x∈y+∞
57 56 ad2antrr ⊢φ∧y∈ℝ∧y<0→x∈x∈A⟼B-1y+∞↔x∈A∧x∈A⟼B⁡x∈y+∞
58 48 53 57 3bitr4d ⊢φ∧y∈ℝ∧y<0→x∈x∈A⟼if0≤−B−B0-1−∞−y↔x∈x∈A⟼B-1y+∞
59 58 alrimiv ⊢φ∧y∈ℝ∧y<0→∀xx∈x∈A⟼if0≤−B−B0-1−∞−y↔x∈x∈A⟼B-1y+∞
60 nfmpt1 ⊢Ⅎ_xx∈A⟼if0≤−B−B0
61 60 nfcnv ⊢Ⅎ_xx∈A⟼if0≤−B−B0-1
62 nfcv ⊢Ⅎ_x−∞−y
63 61 62 nfima ⊢Ⅎ_xx∈A⟼if0≤−B−B0-1−∞−y
64 nfmpt1 ⊢Ⅎ_xx∈A⟼B
65 64 nfcnv ⊢Ⅎ_xx∈A⟼B-1
66 nfcv ⊢Ⅎ_xy+∞
67 65 66 nfima ⊢Ⅎ_xx∈A⟼B-1y+∞
68 63 67 cleqf ⊢x∈A⟼if0≤−B−B0-1−∞−y=x∈A⟼B-1y+∞↔∀xx∈x∈A⟼if0≤−B−B0-1−∞−y↔x∈x∈A⟼B-1y+∞
69 59 68 sylibr ⊢φ∧y∈ℝ∧y<0→x∈A⟼if0≤−B−B0-1−∞−y=x∈A⟼B-1y+∞
70 mbfima ⊢x∈A⟼if0≤−B−B0∈MblFn∧x∈A⟼if0≤−B−B0:A⟶ℝ→x∈A⟼if0≤−B−B0-1−∞−y∈dom⁡vol
71 3 49 70 syl2anc ⊢φ→x∈A⟼if0≤−B−B0-1−∞−y∈dom⁡vol
72 71 ad2antrr ⊢φ∧y∈ℝ∧y<0→x∈A⟼if0≤−B−B0-1−∞−y∈dom⁡vol
73 69 72 eqeltrrd ⊢φ∧y∈ℝ∧y<0→x∈A⟼B-1y+∞∈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∈ℝ→if0≤BB0≤y↔0≤y∧B≤y
79 75 76 77 78 syl3anc ⊢φ∧y∈ℝ∧0≤y∧x∈A→if0≤BB0≤y↔0≤y∧B≤y
80 74 79 mpbirand ⊢φ∧y∈ℝ∧0≤y∧x∈A→if0≤BB0≤y↔B≤y
81 80 notbid ⊢φ∧y∈ℝ∧0≤y∧x∈A→¬if0≤BB0≤y↔¬B≤y
82 76 5 6 sylancl ⊢φ∧y∈ℝ∧0≤y∧x∈A→if0≤BB0∈ℝ
83 77 82 ltnled ⊢φ∧y∈ℝ∧0≤y∧x∈A→y<if0≤BB0↔¬if0≤BB0≤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<if0≤BB0↔y<B
86 82 biantrurd ⊢φ∧y∈ℝ∧0≤y∧x∈A→y<if0≤BB0↔if0≤BB0∈ℝ∧y<if0≤BB0
87 76 biantrurd ⊢φ∧y∈ℝ∧0≤y∧x∈A→y<B↔B∈ℝ∧y<B
88 85 86 87 3bitr3d ⊢φ∧y∈ℝ∧0≤y∧x∈A→if0≤BB0∈ℝ∧y<if0≤BB0↔B∈ℝ∧y<B
89 77 rexrd ⊢φ∧y∈ℝ∧0≤y∧x∈A→y∈ℝ*
90 elioopnf ⊢y∈ℝ*→if0≤BB0∈y+∞↔if0≤BB0∈ℝ∧y<if0≤BB0
91 89 90 syl ⊢φ∧y∈ℝ∧0≤y∧x∈A→if0≤BB0∈y+∞↔if0≤BB0∈ℝ∧y<if0≤BB0
92 89 33 syl ⊢φ∧y∈ℝ∧0≤y∧x∈A→B∈y+∞↔B∈ℝ∧y<B
93 88 91 92 3bitr4d ⊢φ∧y∈ℝ∧0≤y∧x∈A→if0≤BB0∈y+∞↔B∈y+∞
94 eqid ⊢x∈A⟼if0≤BB0=x∈A⟼if0≤BB0
95 94 fvmpt2 ⊢x∈A∧if0≤BB0∈ℝ→x∈A⟼if0≤BB0⁡x=if0≤BB0
96 36 7 95 syl2anc ⊢φ∧x∈A→x∈A⟼if0≤BB0⁡x=if0≤BB0
97 96 eleq1d ⊢φ∧x∈A→x∈A⟼if0≤BB0⁡x∈y+∞↔if0≤BB0∈y+∞
98 97 ad4ant14 ⊢φ∧y∈ℝ∧0≤y∧x∈A→x∈A⟼if0≤BB0⁡x∈y+∞↔if0≤BB0∈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⟼if0≤BB0⁡x∈y+∞↔x∈A⟼B⁡x∈y+∞
101 100 pm5.32da ⊢φ∧y∈ℝ∧0≤y→x∈A∧x∈A⟼if0≤BB0⁡x∈y+∞↔x∈A∧x∈A⟼B⁡x∈y+∞
102 7 fmpttd ⊢φ→x∈A⟼if0≤BB0:A⟶ℝ
103 ffn ⊢x∈A⟼if0≤BB0:A⟶ℝ→x∈A⟼if0≤BB0FnA
104 elpreima ⊢x∈A⟼if0≤BB0FnA→x∈x∈A⟼if0≤BB0-1y+∞↔x∈A∧x∈A⟼if0≤BB0⁡x∈y+∞
105 102 103 104 3syl ⊢φ→x∈x∈A⟼if0≤BB0-1y+∞↔x∈A∧x∈A⟼if0≤BB0⁡x∈y+∞
106 105 ad2antrr ⊢φ∧y∈ℝ∧0≤y→x∈x∈A⟼if0≤BB0-1y+∞↔x∈A∧x∈A⟼if0≤BB0⁡x∈y+∞
107 56 ad2antrr ⊢φ∧y∈ℝ∧0≤y→x∈x∈A⟼B-1y+∞↔x∈A∧x∈A⟼B⁡x∈y+∞
108 101 106 107 3bitr4d ⊢φ∧y∈ℝ∧0≤y→x∈x∈A⟼if0≤BB0-1y+∞↔x∈x∈A⟼B-1y+∞
109 108 alrimiv ⊢φ∧y∈ℝ∧0≤y→∀xx∈x∈A⟼if0≤BB0-1y+∞↔x∈x∈A⟼B-1y+∞
110 nfmpt1 ⊢Ⅎ_xx∈A⟼if0≤BB0
111 110 nfcnv ⊢Ⅎ_xx∈A⟼if0≤BB0-1
112 111 66 nfima ⊢Ⅎ_xx∈A⟼if0≤BB0-1y+∞
113 112 67 cleqf ⊢x∈A⟼if0≤BB0-1y+∞=x∈A⟼B-1y+∞↔∀xx∈x∈A⟼if0≤BB0-1y+∞↔x∈x∈A⟼B-1y+∞
114 109 113 sylibr ⊢φ∧y∈ℝ∧0≤y→x∈A⟼if0≤BB0-1y+∞=x∈A⟼B-1y+∞
115 mbfima ⊢x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤BB0:A⟶ℝ→x∈A⟼if0≤BB0-1y+∞∈dom⁡vol
116 2 102 115 syl2anc ⊢φ→x∈A⟼if0≤BB0-1y+∞∈dom⁡vol
117 116 ad2antrr ⊢φ∧y∈ℝ∧0≤y→x∈A⟼if0≤BB0-1y+∞∈dom⁡vol
118 114 117 eqeltrrd ⊢φ∧y∈ℝ∧0≤y→x∈A⟼B-1y+∞∈dom⁡vol
119 simpr ⊢φ∧y∈ℝ→y∈ℝ
120 0red ⊢φ∧y∈ℝ→0∈ℝ
121 73 118 119 120 ltlecasei ⊢φ∧y∈ℝ→x∈A⟼B-1y+∞∈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∈ℝ→if0≤BB0<y↔0<y∧B<y
127 123 124 125 126 syl3anc ⊢φ∧y∈ℝ∧0<y∧x∈A→if0≤BB0<y↔0<y∧B<y
128 122 127 mpbirand ⊢φ∧y∈ℝ∧0<y∧x∈A→if0≤BB0<y↔B<y
129 7 ad4ant14 ⊢φ∧y∈ℝ∧0<y∧x∈A→if0≤BB0∈ℝ
130 129 biantrurd ⊢φ∧y∈ℝ∧0<y∧x∈A→if0≤BB0<y↔if0≤BB0∈ℝ∧if0≤BB0<y
131 124 biantrurd ⊢φ∧y∈ℝ∧0<y∧x∈A→B<y↔B∈ℝ∧B<y
132 128 130 131 3bitr3d ⊢φ∧y∈ℝ∧0<y∧x∈A→if0≤BB0∈ℝ∧if0≤BB0<y↔B∈ℝ∧B<y
133 125 rexrd ⊢φ∧y∈ℝ∧0<y∧x∈A→y∈ℝ*
134 elioomnf ⊢y∈ℝ*→if0≤BB0∈−∞y↔if0≤BB0∈ℝ∧if0≤BB0<y
135 133 134 syl ⊢φ∧y∈ℝ∧0<y∧x∈A→if0≤BB0∈−∞y↔if0≤BB0∈ℝ∧if0≤BB0<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→if0≤BB0∈−∞y↔B∈−∞y
139 96 eleq1d ⊢φ∧x∈A→x∈A⟼if0≤BB0⁡x∈−∞y↔if0≤BB0∈−∞y
140 139 ad4ant14 ⊢φ∧y∈ℝ∧0<y∧x∈A→x∈A⟼if0≤BB0⁡x∈−∞y↔if0≤BB0∈−∞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⟼if0≤BB0⁡x∈−∞y↔x∈A⟼B⁡x∈−∞y
144 143 pm5.32da ⊢φ∧y∈ℝ∧0<y→x∈A∧x∈A⟼if0≤BB0⁡x∈−∞y↔x∈A∧x∈A⟼B⁡x∈−∞y
145 elpreima ⊢x∈A⟼if0≤BB0FnA→x∈x∈A⟼if0≤BB0-1−∞y↔x∈A∧x∈A⟼if0≤BB0⁡x∈−∞y
146 102 103 145 3syl ⊢φ→x∈x∈A⟼if0≤BB0-1−∞y↔x∈A∧x∈A⟼if0≤BB0⁡x∈−∞y
147 146 ad2antrr ⊢φ∧y∈ℝ∧0<y→x∈x∈A⟼if0≤BB0-1−∞y↔x∈A∧x∈A⟼if0≤BB0⁡x∈−∞y
148 elpreima ⊢x∈A⟼BFnA→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⟼if0≤BB0-1−∞y↔x∈x∈A⟼B-1−∞y
152 151 alrimiv ⊢φ∧y∈ℝ∧0<y→∀xx∈x∈A⟼if0≤BB0-1−∞y↔x∈x∈A⟼B-1−∞y
153 nfcv ⊢Ⅎ_x−∞y
154 111 153 nfima ⊢Ⅎ_xx∈A⟼if0≤BB0-1−∞y
155 65 153 nfima ⊢Ⅎ_xx∈A⟼B-1−∞y
156 154 155 cleqf ⊢x∈A⟼if0≤BB0-1−∞y=x∈A⟼B-1−∞y↔∀xx∈x∈A⟼if0≤BB0-1−∞y↔x∈x∈A⟼B-1−∞y
157 152 156 sylibr ⊢φ∧y∈ℝ∧0<y→x∈A⟼if0≤BB0-1−∞y=x∈A⟼B-1−∞y
158 mbfima ⊢x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤BB0:A⟶ℝ→x∈A⟼if0≤BB0-1−∞y∈dom⁡vol
159 2 102 158 syl2anc ⊢φ→x∈A⟼if0≤BB0-1−∞y∈dom⁡vol
160 159 ad2antrr ⊢φ∧y∈ℝ∧0<y→x∈A⟼if0≤BB0-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∈ℝ→if0≤−B−B0≤−y↔0≤−y∧−B≤−y
173 169 170 171 172 syl3anc ⊢φ∧y∈ℝ∧y≤0∧x∈A→if0≤−B−B0≤−y↔0≤−y∧−B≤−y
174 166 168 173 3bitr4rd ⊢φ∧y∈ℝ∧y≤0∧x∈A→if0≤−B−B0≤−y↔y≤B
175 174 notbid ⊢φ∧y∈ℝ∧y≤0∧x∈A→¬if0≤−B−B0≤−y↔¬y≤B
176 24 ad4ant14 ⊢φ∧y∈ℝ∧y≤0∧x∈A→if0≤−B−B0∈ℝ
177 171 176 ltnled ⊢φ∧y∈ℝ∧y≤0∧x∈A→−y<if0≤−B−B0↔¬if0≤−B−B0≤−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<if0≤−B−B0↔B<y
180 176 biantrurd ⊢φ∧y∈ℝ∧y≤0∧x∈A→−y<if0≤−B−B0↔if0≤−B−B0∈ℝ∧−y<if0≤−B−B0
181 167 biantrurd ⊢φ∧y∈ℝ∧y≤0∧x∈A→B<y↔B∈ℝ∧B<y
182 179 180 181 3bitr3d ⊢φ∧y∈ℝ∧y≤0∧x∈A→if0≤−B−B0∈ℝ∧−y<if0≤−B−B0↔B∈ℝ∧B<y
183 171 rexrd ⊢φ∧y∈ℝ∧y≤0∧x∈A→−y∈ℝ*
184 elioopnf ⊢−y∈ℝ*→if0≤−B−B0∈−y+∞↔if0≤−B−B0∈ℝ∧−y<if0≤−B−B0
185 183 184 syl ⊢φ∧y∈ℝ∧y≤0∧x∈A→if0≤−B−B0∈−y+∞↔if0≤−B−B0∈ℝ∧−y<if0≤−B−B0
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→if0≤−B−B0∈−y+∞↔B∈−∞y
189 39 eleq1d ⊢φ∧x∈A→x∈A⟼if0≤−B−B0⁡x∈−y+∞↔if0≤−B−B0∈−y+∞
190 189 ad4ant14 ⊢φ∧y∈ℝ∧y≤0∧x∈A→x∈A⟼if0≤−B−B0⁡x∈−y+∞↔if0≤−B−B0∈−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⟼if0≤−B−B0⁡x∈−y+∞↔x∈A⟼B⁡x∈−∞y
193 192 pm5.32da ⊢φ∧y∈ℝ∧y≤0→x∈A∧x∈A⟼if0≤−B−B0⁡x∈−y+∞↔x∈A∧x∈A⟼B⁡x∈−∞y
194 elpreima ⊢x∈A⟼if0≤−B−B0FnA→x∈x∈A⟼if0≤−B−B0-1−y+∞↔x∈A∧x∈A⟼if0≤−B−B0⁡x∈−y+∞
195 49 50 194 3syl ⊢φ→x∈x∈A⟼if0≤−B−B0-1−y+∞↔x∈A∧x∈A⟼if0≤−B−B0⁡x∈−y+∞
196 195 ad2antrr ⊢φ∧y∈ℝ∧y≤0→x∈x∈A⟼if0≤−B−B0-1−y+∞↔x∈A∧x∈A⟼if0≤−B−B0⁡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⟼if0≤−B−B0-1−y+∞↔x∈x∈A⟼B-1−∞y
199 198 alrimiv ⊢φ∧y∈ℝ∧y≤0→∀xx∈x∈A⟼if0≤−B−B0-1−y+∞↔x∈x∈A⟼B-1−∞y
200 nfcv ⊢Ⅎ_x−y+∞
201 61 200 nfima ⊢Ⅎ_xx∈A⟼if0≤−B−B0-1−y+∞
202 201 155 cleqf ⊢x∈A⟼if0≤−B−B0-1−y+∞=x∈A⟼B-1−∞y↔∀xx∈x∈A⟼if0≤−B−B0-1−y+∞↔x∈x∈A⟼B-1−∞y
203 199 202 sylibr ⊢φ∧y∈ℝ∧y≤0→x∈A⟼if0≤−B−B0-1−y+∞=x∈A⟼B-1−∞y
204 mbfima ⊢x∈A⟼if0≤−B−B0∈MblFn∧x∈A⟼if0≤−B−B0:A⟶ℝ→x∈A⟼if0≤−B−B0-1−y+∞∈dom⁡vol
205 3 49 204 syl2anc ⊢φ→x∈A⟼if0≤−B−B0-1−y+∞∈dom⁡vol
206 205 ad2antrr ⊢φ∧y∈ℝ∧y≤0→x∈A⟼if0≤−B−B0-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