Step |
Hyp |
Ref |
Expression |
1 |
|
nsssmfmbflem.s |
|- S = dom vol |
2 |
|
nsssmfmbflem.x |
|- ( ph -> X C_ RR ) |
3 |
|
nsssmfmbflem.n |
|- ( ph -> -. X e. S ) |
4 |
|
nsssmfmbflem.f |
|- F = ( x e. X |-> 0 ) |
5 |
|
0red |
|- ( ( ph /\ x e. X ) -> 0 e. RR ) |
6 |
5 4
|
fmptd |
|- ( ph -> F : X --> RR ) |
7 |
|
reex |
|- RR e. _V |
8 |
7
|
a1i |
|- ( ph -> RR e. _V ) |
9 |
8 2
|
ssexd |
|- ( ph -> X e. _V ) |
10 |
6 9
|
fexd |
|- ( ph -> F e. _V ) |
11 |
1 2 3 4
|
smfmbfcex |
|- ( ph -> ( F e. ( SMblFn ` S ) /\ -. F e. MblFn ) ) |
12 |
|
eleq1 |
|- ( f = F -> ( f e. ( SMblFn ` S ) <-> F e. ( SMblFn ` S ) ) ) |
13 |
|
eleq1 |
|- ( f = F -> ( f e. MblFn <-> F e. MblFn ) ) |
14 |
13
|
notbid |
|- ( f = F -> ( -. f e. MblFn <-> -. F e. MblFn ) ) |
15 |
12 14
|
anbi12d |
|- ( f = F -> ( ( f e. ( SMblFn ` S ) /\ -. f e. MblFn ) <-> ( F e. ( SMblFn ` S ) /\ -. F e. MblFn ) ) ) |
16 |
15
|
spcegv |
|- ( F e. _V -> ( ( F e. ( SMblFn ` S ) /\ -. F e. MblFn ) -> E. f ( f e. ( SMblFn ` S ) /\ -. f e. MblFn ) ) ) |
17 |
10 11 16
|
sylc |
|- ( ph -> E. f ( f e. ( SMblFn ` S ) /\ -. f e. MblFn ) ) |