Step |
Hyp |
Ref |
Expression |
1 |
|
reex |
|- RR e. _V |
2 |
1
|
pwex |
|- ~P RR e. _V |
3 |
|
dmvolss |
|- dom vol C_ ~P RR |
4 |
2 3
|
ssexi |
|- dom vol e. _V |
5 |
4
|
a1i |
|- ( T. -> dom vol e. _V ) |
6 |
|
0mbl |
|- (/) e. dom vol |
7 |
6
|
a1i |
|- ( T. -> (/) e. dom vol ) |
8 |
|
unidmvol |
|- U. dom vol = RR |
9 |
8
|
eqcomi |
|- RR = U. dom vol |
10 |
|
cmmbl |
|- ( y e. dom vol -> ( RR \ y ) e. dom vol ) |
11 |
10
|
adantl |
|- ( ( T. /\ y e. dom vol ) -> ( RR \ y ) e. dom vol ) |
12 |
|
ffvelrn |
|- ( ( e : NN --> dom vol /\ n e. NN ) -> ( e ` n ) e. dom vol ) |
13 |
12
|
ralrimiva |
|- ( e : NN --> dom vol -> A. n e. NN ( e ` n ) e. dom vol ) |
14 |
|
iunmbl |
|- ( A. n e. NN ( e ` n ) e. dom vol -> U_ n e. NN ( e ` n ) e. dom vol ) |
15 |
13 14
|
syl |
|- ( e : NN --> dom vol -> U_ n e. NN ( e ` n ) e. dom vol ) |
16 |
15
|
adantl |
|- ( ( T. /\ e : NN --> dom vol ) -> U_ n e. NN ( e ` n ) e. dom vol ) |
17 |
5 7 9 11 16
|
issalnnd |
|- ( T. -> dom vol e. SAlg ) |
18 |
17
|
mptru |
|- dom vol e. SAlg |