Database
BASIC REAL AND COMPLEX ANALYSIS
Integrals
Lebesgue integration
Lesbesgue integral
ismbf3d
Next ⟩
mbfimaopnlem
Metamath Proof Explorer
Ascii
Unicode
Theorem
ismbf3d
Description:
Simplified form of
ismbfd
.
(Contributed by
Mario Carneiro
, 18-Jun-2014)
Ref
Expression
Hypotheses
ismbf3d.1
⊢
φ
→
F
:
A
⟶
ℝ
ismbf3d.2
⊢
φ
∧
x
∈
ℝ
→
F
-1
x
+∞
∈
dom
vol
Assertion
ismbf3d
⊢
φ
→
F
∈
MblFn
Proof
Step
Hyp
Ref
Expression
1
ismbf3d.1
⊢
φ
→
F
:
A
⟶
ℝ
2
ismbf3d.2
⊢
φ
∧
x
∈
ℝ
→
F
-1
x
+∞
∈
dom
vol
3
fimacnv
⊢
F
:
A
⟶
ℝ
→
F
-1
ℝ
=
A
4
1
3
syl
⊢
φ
→
F
-1
ℝ
=
A
5
imaiun
⊢
F
-1
⋃
y
∈
ℕ
−
y
+∞
=
⋃
y
∈
ℕ
F
-1
−
y
+∞
6
ioossre
⊢
−
y
+∞
⊆
ℝ
7
6
rgenw
⊢
∀
y
∈
ℕ
−
y
+∞
⊆
ℝ
8
iunss
⊢
⋃
y
∈
ℕ
−
y
+∞
⊆
ℝ
↔
∀
y
∈
ℕ
−
y
+∞
⊆
ℝ
9
7
8
mpbir
⊢
⋃
y
∈
ℕ
−
y
+∞
⊆
ℝ
10
renegcl
⊢
z
∈
ℝ
→
−
z
∈
ℝ
11
arch
⊢
−
z
∈
ℝ
→
∃
y
∈
ℕ
−
z
<
y
12
10
11
syl
⊢
z
∈
ℝ
→
∃
y
∈
ℕ
−
z
<
y
13
simpl
⊢
z
∈
ℝ
∧
y
∈
ℕ
→
z
∈
ℝ
14
13
biantrurd
⊢
z
∈
ℝ
∧
y
∈
ℕ
→
−
y
<
z
↔
z
∈
ℝ
∧
−
y
<
z
15
nnre
⊢
y
∈
ℕ
→
y
∈
ℝ
16
ltnegcon1
⊢
z
∈
ℝ
∧
y
∈
ℝ
→
−
z
<
y
↔
−
y
<
z
17
15
16
sylan2
⊢
z
∈
ℝ
∧
y
∈
ℕ
→
−
z
<
y
↔
−
y
<
z
18
15
adantl
⊢
z
∈
ℝ
∧
y
∈
ℕ
→
y
∈
ℝ
19
18
renegcld
⊢
z
∈
ℝ
∧
y
∈
ℕ
→
−
y
∈
ℝ
20
19
rexrd
⊢
z
∈
ℝ
∧
y
∈
ℕ
→
−
y
∈
ℝ
*
21
elioopnf
⊢
−
y
∈
ℝ
*
→
z
∈
−
y
+∞
↔
z
∈
ℝ
∧
−
y
<
z
22
20
21
syl
⊢
z
∈
ℝ
∧
y
∈
ℕ
→
z
∈
−
y
+∞
↔
z
∈
ℝ
∧
−
y
<
z
23
14
17
22
3bitr4d
⊢
z
∈
ℝ
∧
y
∈
ℕ
→
−
z
<
y
↔
z
∈
−
y
+∞
24
23
rexbidva
⊢
z
∈
ℝ
→
∃
y
∈
ℕ
−
z
<
y
↔
∃
y
∈
ℕ
z
∈
−
y
+∞
25
12
24
mpbid
⊢
z
∈
ℝ
→
∃
y
∈
ℕ
z
∈
−
y
+∞
26
eliun
⊢
z
∈
⋃
y
∈
ℕ
−
y
+∞
↔
∃
y
∈
ℕ
z
∈
−
y
+∞
27
25
26
sylibr
⊢
z
∈
ℝ
→
z
∈
⋃
y
∈
ℕ
−
y
+∞
28
27
ssriv
⊢
ℝ
⊆
⋃
y
∈
ℕ
−
y
+∞
29
9
28
eqssi
⊢
⋃
y
∈
ℕ
−
y
+∞
=
ℝ
30
29
imaeq2i
⊢
F
-1
⋃
y
∈
ℕ
−
y
+∞
=
F
-1
ℝ
31
5
30
eqtr3i
⊢
⋃
y
∈
ℕ
F
-1
−
y
+∞
=
F
-1
ℝ
32
2
ralrimiva
⊢
φ
→
∀
x
∈
ℝ
F
-1
x
+∞
∈
dom
vol
33
15
renegcld
⊢
y
∈
ℕ
→
−
y
∈
ℝ
34
oveq1
⊢
x
=
−
y
→
x
+∞
=
−
y
+∞
35
34
imaeq2d
⊢
x
=
−
y
→
F
-1
x
+∞
=
F
-1
−
y
+∞
36
35
eleq1d
⊢
x
=
−
y
→
F
-1
x
+∞
∈
dom
vol
↔
F
-1
−
y
+∞
∈
dom
vol
37
36
rspccva
⊢
∀
x
∈
ℝ
F
-1
x
+∞
∈
dom
vol
∧
−
y
∈
ℝ
→
F
-1
−
y
+∞
∈
dom
vol
38
32
33
37
syl2an
⊢
φ
∧
y
∈
ℕ
→
F
-1
−
y
+∞
∈
dom
vol
39
38
ralrimiva
⊢
φ
→
∀
y
∈
ℕ
F
-1
−
y
+∞
∈
dom
vol
40
iunmbl
⊢
∀
y
∈
ℕ
F
-1
−
y
+∞
∈
dom
vol
→
⋃
y
∈
ℕ
F
-1
−
y
+∞
∈
dom
vol
41
39
40
syl
⊢
φ
→
⋃
y
∈
ℕ
F
-1
−
y
+∞
∈
dom
vol
42
31
41
eqeltrrid
⊢
φ
→
F
-1
ℝ
∈
dom
vol
43
4
42
eqeltrrd
⊢
φ
→
A
∈
dom
vol
44
imaiun
⊢
F
-1
⋃
y
∈
ℕ
−∞
z
−
1
y
=
⋃
y
∈
ℕ
F
-1
−∞
z
−
1
y
45
eliun
⊢
x
∈
⋃
y
∈
ℕ
−∞
z
−
1
y
↔
∃
y
∈
ℕ
x
∈
−∞
z
−
1
y
46
3simpb
⊢
x
∈
ℝ
∧
−∞
<
x
∧
x
≤
z
−
1
y
→
x
∈
ℝ
∧
x
≤
z
−
1
y
47
simplr
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
∧
x
∈
ℝ
→
z
∈
ℝ
48
nnrp
⊢
y
∈
ℕ
→
y
∈
ℝ
+
49
48
ad2antrl
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
∧
x
∈
ℝ
→
y
∈
ℝ
+
50
49
rpreccld
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
∧
x
∈
ℝ
→
1
y
∈
ℝ
+
51
47
50
ltsubrpd
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
∧
x
∈
ℝ
→
z
−
1
y
<
z
52
simprr
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
∧
x
∈
ℝ
→
x
∈
ℝ
53
simpr
⊢
φ
∧
z
∈
ℝ
→
z
∈
ℝ
54
nnrecre
⊢
y
∈
ℕ
→
1
y
∈
ℝ
55
resubcl
⊢
z
∈
ℝ
∧
1
y
∈
ℝ
→
z
−
1
y
∈
ℝ
56
53
54
55
syl2an
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
z
−
1
y
∈
ℝ
57
56
adantrr
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
∧
x
∈
ℝ
→
z
−
1
y
∈
ℝ
58
lelttr
⊢
x
∈
ℝ
∧
z
−
1
y
∈
ℝ
∧
z
∈
ℝ
→
x
≤
z
−
1
y
∧
z
−
1
y
<
z
→
x
<
z
59
52
57
47
58
syl3anc
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
∧
x
∈
ℝ
→
x
≤
z
−
1
y
∧
z
−
1
y
<
z
→
x
<
z
60
51
59
mpan2d
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
∧
x
∈
ℝ
→
x
≤
z
−
1
y
→
x
<
z
61
60
anassrs
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
∧
x
∈
ℝ
→
x
≤
z
−
1
y
→
x
<
z
62
61
imdistanda
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
x
∈
ℝ
∧
x
≤
z
−
1
y
→
x
∈
ℝ
∧
x
<
z
63
46
62
syl5
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
x
∈
ℝ
∧
−∞
<
x
∧
x
≤
z
−
1
y
→
x
∈
ℝ
∧
x
<
z
64
mnfxr
⊢
−∞
∈
ℝ
*
65
elioc2
⊢
−∞
∈
ℝ
*
∧
z
−
1
y
∈
ℝ
→
x
∈
−∞
z
−
1
y
↔
x
∈
ℝ
∧
−∞
<
x
∧
x
≤
z
−
1
y
66
64
56
65
sylancr
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
x
∈
−∞
z
−
1
y
↔
x
∈
ℝ
∧
−∞
<
x
∧
x
≤
z
−
1
y
67
rexr
⊢
z
∈
ℝ
→
z
∈
ℝ
*
68
67
adantl
⊢
φ
∧
z
∈
ℝ
→
z
∈
ℝ
*
69
elioomnf
⊢
z
∈
ℝ
*
→
x
∈
−∞
z
↔
x
∈
ℝ
∧
x
<
z
70
68
69
syl
⊢
φ
∧
z
∈
ℝ
→
x
∈
−∞
z
↔
x
∈
ℝ
∧
x
<
z
71
70
adantr
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
x
∈
−∞
z
↔
x
∈
ℝ
∧
x
<
z
72
63
66
71
3imtr4d
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
x
∈
−∞
z
−
1
y
→
x
∈
−∞
z
73
72
rexlimdva
⊢
φ
∧
z
∈
ℝ
→
∃
y
∈
ℕ
x
∈
−∞
z
−
1
y
→
x
∈
−∞
z
74
73
70
sylibd
⊢
φ
∧
z
∈
ℝ
→
∃
y
∈
ℕ
x
∈
−∞
z
−
1
y
→
x
∈
ℝ
∧
x
<
z
75
simprl
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
→
x
∈
ℝ
76
75
adantr
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
x
∈
ℝ
77
76
mnfltd
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
−∞
<
x
78
56
ad2ant2r
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
z
−
1
y
∈
ℝ
79
54
ad2antrl
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
1
y
∈
ℝ
80
simplr
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
→
z
∈
ℝ
81
80
adantr
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
z
∈
ℝ
82
simprr
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
1
y
<
z
−
x
83
79
81
76
82
ltsub13d
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
x
<
z
−
1
y
84
76
78
83
ltled
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
x
≤
z
−
1
y
85
66
ad2ant2r
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
x
∈
−∞
z
−
1
y
↔
x
∈
ℝ
∧
−∞
<
x
∧
x
≤
z
−
1
y
86
76
77
84
85
mpbir3and
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
∧
y
∈
ℕ
∧
1
y
<
z
−
x
→
x
∈
−∞
z
−
1
y
87
80
75
resubcld
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
→
z
−
x
∈
ℝ
88
simprr
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
→
x
<
z
89
75
80
posdifd
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
→
x
<
z
↔
0
<
z
−
x
90
88
89
mpbid
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
→
0
<
z
−
x
91
nnrecl
⊢
z
−
x
∈
ℝ
∧
0
<
z
−
x
→
∃
y
∈
ℕ
1
y
<
z
−
x
92
87
90
91
syl2anc
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
→
∃
y
∈
ℕ
1
y
<
z
−
x
93
86
92
reximddv
⊢
φ
∧
z
∈
ℝ
∧
x
∈
ℝ
∧
x
<
z
→
∃
y
∈
ℕ
x
∈
−∞
z
−
1
y
94
93
ex
⊢
φ
∧
z
∈
ℝ
→
x
∈
ℝ
∧
x
<
z
→
∃
y
∈
ℕ
x
∈
−∞
z
−
1
y
95
74
94
impbid
⊢
φ
∧
z
∈
ℝ
→
∃
y
∈
ℕ
x
∈
−∞
z
−
1
y
↔
x
∈
ℝ
∧
x
<
z
96
95
70
bitr4d
⊢
φ
∧
z
∈
ℝ
→
∃
y
∈
ℕ
x
∈
−∞
z
−
1
y
↔
x
∈
−∞
z
97
45
96
syl5bb
⊢
φ
∧
z
∈
ℝ
→
x
∈
⋃
y
∈
ℕ
−∞
z
−
1
y
↔
x
∈
−∞
z
98
97
eqrdv
⊢
φ
∧
z
∈
ℝ
→
⋃
y
∈
ℕ
−∞
z
−
1
y
=
−∞
z
99
98
imaeq2d
⊢
φ
∧
z
∈
ℝ
→
F
-1
⋃
y
∈
ℕ
−∞
z
−
1
y
=
F
-1
−∞
z
100
44
99
eqtr3id
⊢
φ
∧
z
∈
ℝ
→
⋃
y
∈
ℕ
F
-1
−∞
z
−
1
y
=
F
-1
−∞
z
101
1
ad2antrr
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
F
:
A
⟶
ℝ
102
ffun
⊢
F
:
A
⟶
ℝ
→
Fun
F
103
funcnvcnv
⊢
Fun
F
→
Fun
F
-1
-1
104
imadif
⊢
Fun
F
-1
-1
→
F
-1
ℝ
∖
z
−
1
y
+∞
=
F
-1
ℝ
∖
F
-1
z
−
1
y
+∞
105
101
102
103
104
4syl
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
F
-1
ℝ
∖
z
−
1
y
+∞
=
F
-1
ℝ
∖
F
-1
z
−
1
y
+∞
106
64
a1i
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
−∞
∈
ℝ
*
107
56
rexrd
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
z
−
1
y
∈
ℝ
*
108
pnfxr
⊢
+∞
∈
ℝ
*
109
108
a1i
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
+∞
∈
ℝ
*
110
56
mnfltd
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
−∞
<
z
−
1
y
111
56
ltpnfd
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
z
−
1
y
<
+∞
112
df-ioc
⊢
.
=
u
∈
ℝ
*
,
v
∈
ℝ
*
⟼
w
∈
ℝ
*
|
u
<
w
∧
w
≤
v
113
df-ioo
⊢
.
=
u
∈
ℝ
*
,
v
∈
ℝ
*
⟼
w
∈
ℝ
*
|
u
<
w
∧
w
<
v
114
xrltnle
⊢
z
−
1
y
∈
ℝ
*
∧
x
∈
ℝ
*
→
z
−
1
y
<
x
↔
¬
x
≤
z
−
1
y
115
xrlelttr
⊢
x
∈
ℝ
*
∧
z
−
1
y
∈
ℝ
*
∧
+∞
∈
ℝ
*
→
x
≤
z
−
1
y
∧
z
−
1
y
<
+∞
→
x
<
+∞
116
xrlttr
⊢
−∞
∈
ℝ
*
∧
z
−
1
y
∈
ℝ
*
∧
x
∈
ℝ
*
→
−∞
<
z
−
1
y
∧
z
−
1
y
<
x
→
−∞
<
x
117
112
113
114
113
115
116
ixxun
⊢
−∞
∈
ℝ
*
∧
z
−
1
y
∈
ℝ
*
∧
+∞
∈
ℝ
*
∧
−∞
<
z
−
1
y
∧
z
−
1
y
<
+∞
→
−∞
z
−
1
y
∪
z
−
1
y
+∞
=
−∞
+∞
118
106
107
109
110
111
117
syl32anc
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
−∞
z
−
1
y
∪
z
−
1
y
+∞
=
−∞
+∞
119
uncom
⊢
−∞
z
−
1
y
∪
z
−
1
y
+∞
=
z
−
1
y
+∞
∪
−∞
z
−
1
y
120
ioomax
⊢
−∞
+∞
=
ℝ
121
118
119
120
3eqtr3g
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
z
−
1
y
+∞
∪
−∞
z
−
1
y
=
ℝ
122
ioossre
⊢
z
−
1
y
+∞
⊆
ℝ
123
incom
⊢
z
−
1
y
+∞
∩
−∞
z
−
1
y
=
−∞
z
−
1
y
∩
z
−
1
y
+∞
124
112
113
114
ixxdisj
⊢
−∞
∈
ℝ
*
∧
z
−
1
y
∈
ℝ
*
∧
+∞
∈
ℝ
*
→
−∞
z
−
1
y
∩
z
−
1
y
+∞
=
∅
125
64
108
124
mp3an13
⊢
z
−
1
y
∈
ℝ
*
→
−∞
z
−
1
y
∩
z
−
1
y
+∞
=
∅
126
107
125
syl
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
−∞
z
−
1
y
∩
z
−
1
y
+∞
=
∅
127
123
126
eqtrid
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
z
−
1
y
+∞
∩
−∞
z
−
1
y
=
∅
128
uneqdifeq
⊢
z
−
1
y
+∞
⊆
ℝ
∧
z
−
1
y
+∞
∩
−∞
z
−
1
y
=
∅
→
z
−
1
y
+∞
∪
−∞
z
−
1
y
=
ℝ
↔
ℝ
∖
z
−
1
y
+∞
=
−∞
z
−
1
y
129
122
127
128
sylancr
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
z
−
1
y
+∞
∪
−∞
z
−
1
y
=
ℝ
↔
ℝ
∖
z
−
1
y
+∞
=
−∞
z
−
1
y
130
121
129
mpbid
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
ℝ
∖
z
−
1
y
+∞
=
−∞
z
−
1
y
131
130
imaeq2d
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
F
-1
ℝ
∖
z
−
1
y
+∞
=
F
-1
−∞
z
−
1
y
132
105
131
eqtr3d
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
F
-1
ℝ
∖
F
-1
z
−
1
y
+∞
=
F
-1
−∞
z
−
1
y
133
42
ad2antrr
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
F
-1
ℝ
∈
dom
vol
134
oveq1
⊢
x
=
z
−
1
y
→
x
+∞
=
z
−
1
y
+∞
135
134
imaeq2d
⊢
x
=
z
−
1
y
→
F
-1
x
+∞
=
F
-1
z
−
1
y
+∞
136
135
eleq1d
⊢
x
=
z
−
1
y
→
F
-1
x
+∞
∈
dom
vol
↔
F
-1
z
−
1
y
+∞
∈
dom
vol
137
32
ad2antrr
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
∀
x
∈
ℝ
F
-1
x
+∞
∈
dom
vol
138
136
137
56
rspcdva
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
F
-1
z
−
1
y
+∞
∈
dom
vol
139
difmbl
⊢
F
-1
ℝ
∈
dom
vol
∧
F
-1
z
−
1
y
+∞
∈
dom
vol
→
F
-1
ℝ
∖
F
-1
z
−
1
y
+∞
∈
dom
vol
140
133
138
139
syl2anc
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
F
-1
ℝ
∖
F
-1
z
−
1
y
+∞
∈
dom
vol
141
132
140
eqeltrrd
⊢
φ
∧
z
∈
ℝ
∧
y
∈
ℕ
→
F
-1
−∞
z
−
1
y
∈
dom
vol
142
141
ralrimiva
⊢
φ
∧
z
∈
ℝ
→
∀
y
∈
ℕ
F
-1
−∞
z
−
1
y
∈
dom
vol
143
iunmbl
⊢
∀
y
∈
ℕ
F
-1
−∞
z
−
1
y
∈
dom
vol
→
⋃
y
∈
ℕ
F
-1
−∞
z
−
1
y
∈
dom
vol
144
142
143
syl
⊢
φ
∧
z
∈
ℝ
→
⋃
y
∈
ℕ
F
-1
−∞
z
−
1
y
∈
dom
vol
145
100
144
eqeltrrd
⊢
φ
∧
z
∈
ℝ
→
F
-1
−∞
z
∈
dom
vol
146
145
ralrimiva
⊢
φ
→
∀
z
∈
ℝ
F
-1
−∞
z
∈
dom
vol
147
oveq2
⊢
z
=
x
→
−∞
z
=
−∞
x
148
147
imaeq2d
⊢
z
=
x
→
F
-1
−∞
z
=
F
-1
−∞
x
149
148
eleq1d
⊢
z
=
x
→
F
-1
−∞
z
∈
dom
vol
↔
F
-1
−∞
x
∈
dom
vol
150
149
cbvralvw
⊢
∀
z
∈
ℝ
F
-1
−∞
z
∈
dom
vol
↔
∀
x
∈
ℝ
F
-1
−∞
x
∈
dom
vol
151
146
150
sylib
⊢
φ
→
∀
x
∈
ℝ
F
-1
−∞
x
∈
dom
vol
152
151
r19.21bi
⊢
φ
∧
x
∈
ℝ
→
F
-1
−∞
x
∈
dom
vol
153
1
43
2
152
ismbf2d
⊢
φ
→
F
∈
MblFn