Step |
Hyp |
Ref |
Expression |
1 |
|
omecl.o |
|- ( ph -> O e. OutMeas ) |
2 |
|
omecl.x |
|- X = U. dom O |
3 |
|
omecl.ss |
|- ( ph -> A C_ X ) |
4 |
1 2
|
omef |
|- ( ph -> O : ~P X --> ( 0 [,] +oo ) ) |
5 |
2
|
a1i |
|- ( ph -> X = U. dom O ) |
6 |
1
|
dmexd |
|- ( ph -> dom O e. _V ) |
7 |
6
|
uniexd |
|- ( ph -> U. dom O e. _V ) |
8 |
5 7
|
eqeltrd |
|- ( ph -> X e. _V ) |
9 |
8 3
|
ssexd |
|- ( ph -> A e. _V ) |
10 |
|
elpwg |
|- ( A e. _V -> ( A e. ~P X <-> A C_ X ) ) |
11 |
9 10
|
syl |
|- ( ph -> ( A e. ~P X <-> A C_ X ) ) |
12 |
3 11
|
mpbird |
|- ( ph -> A e. ~P X ) |
13 |
4 12
|
ffvelrnd |
|- ( ph -> ( O ` A ) e. ( 0 [,] +oo ) ) |