Step |
Hyp |
Ref |
Expression |
1 |
|
pwsiga |
|- ( O e. V -> ~P O e. ( sigAlgebra ` O ) ) |
2 |
|
elrnsiga |
|- ( ~P O e. ( sigAlgebra ` O ) -> ~P O e. U. ran sigAlgebra ) |
3 |
1 2
|
syl |
|- ( O e. V -> ~P O e. U. ran sigAlgebra ) |
4 |
|
brsigarn |
|- BrSiga e. ( sigAlgebra ` RR ) |
5 |
|
elrnsiga |
|- ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra ) |
6 |
4 5
|
mp1i |
|- ( O e. V -> BrSiga e. U. ran sigAlgebra ) |
7 |
3 6
|
ismbfm |
|- ( O e. V -> ( f e. ( ~P O MblFnM BrSiga ) <-> ( f e. ( U. BrSiga ^m U. ~P O ) /\ A. x e. BrSiga ( `' f " x ) e. ~P O ) ) ) |
8 |
|
unibrsiga |
|- U. BrSiga = RR |
9 |
|
reex |
|- RR e. _V |
10 |
8 9
|
eqeltri |
|- U. BrSiga e. _V |
11 |
|
unipw |
|- U. ~P O = O |
12 |
|
elex |
|- ( O e. V -> O e. _V ) |
13 |
11 12
|
eqeltrid |
|- ( O e. V -> U. ~P O e. _V ) |
14 |
|
elmapg |
|- ( ( U. BrSiga e. _V /\ U. ~P O e. _V ) -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> f : U. ~P O --> U. BrSiga ) ) |
15 |
10 13 14
|
sylancr |
|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> f : U. ~P O --> U. BrSiga ) ) |
16 |
11
|
feq2i |
|- ( f : U. ~P O --> U. BrSiga <-> f : O --> U. BrSiga ) |
17 |
15 16
|
syl6bb |
|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> f : O --> U. BrSiga ) ) |
18 |
|
ffn |
|- ( f : O --> U. BrSiga -> f Fn O ) |
19 |
17 18
|
syl6bi |
|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) -> f Fn O ) ) |
20 |
|
elpreima |
|- ( f Fn O -> ( y e. ( `' f " x ) <-> ( y e. O /\ ( f ` y ) e. x ) ) ) |
21 |
|
simpl |
|- ( ( y e. O /\ ( f ` y ) e. x ) -> y e. O ) |
22 |
20 21
|
syl6bi |
|- ( f Fn O -> ( y e. ( `' f " x ) -> y e. O ) ) |
23 |
22
|
ssrdv |
|- ( f Fn O -> ( `' f " x ) C_ O ) |
24 |
|
vex |
|- f e. _V |
25 |
24
|
cnvex |
|- `' f e. _V |
26 |
|
imaexg |
|- ( `' f e. _V -> ( `' f " x ) e. _V ) |
27 |
25 26
|
ax-mp |
|- ( `' f " x ) e. _V |
28 |
27
|
elpw |
|- ( ( `' f " x ) e. ~P O <-> ( `' f " x ) C_ O ) |
29 |
23 28
|
sylibr |
|- ( f Fn O -> ( `' f " x ) e. ~P O ) |
30 |
29
|
ralrimivw |
|- ( f Fn O -> A. x e. BrSiga ( `' f " x ) e. ~P O ) |
31 |
19 30
|
syl6 |
|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) -> A. x e. BrSiga ( `' f " x ) e. ~P O ) ) |
32 |
31
|
pm4.71d |
|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> ( f e. ( U. BrSiga ^m U. ~P O ) /\ A. x e. BrSiga ( `' f " x ) e. ~P O ) ) ) |
33 |
7 32
|
bitr4d |
|- ( O e. V -> ( f e. ( ~P O MblFnM BrSiga ) <-> f e. ( U. BrSiga ^m U. ~P O ) ) ) |
34 |
33
|
eqrdv |
|- ( O e. V -> ( ~P O MblFnM BrSiga ) = ( U. BrSiga ^m U. ~P O ) ) |
35 |
8 11
|
oveq12i |
|- ( U. BrSiga ^m U. ~P O ) = ( RR ^m O ) |
36 |
34 35
|
eqtrdi |
|- ( O e. V -> ( ~P O MblFnM BrSiga ) = ( RR ^m O ) ) |