Step |
Hyp |
Ref |
Expression |
1 |
|
mulex |
|- x. e. _V |
2 |
|
cnfldstr |
|- CCfld Struct <. 1 , ; 1 3 >. |
3 |
|
mulrid |
|- .r = Slot ( .r ` ndx ) |
4 |
|
snsstp3 |
|- { <. ( .r ` ndx ) , x. >. } C_ { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } |
5 |
|
ssun1 |
|- { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } C_ ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) |
6 |
|
ssun1 |
|- ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) C_ ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) |
7 |
|
df-cnfld |
|- CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) |
8 |
6 7
|
sseqtrri |
|- ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) C_ CCfld |
9 |
5 8
|
sstri |
|- { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } C_ CCfld |
10 |
4 9
|
sstri |
|- { <. ( .r ` ndx ) , x. >. } C_ CCfld |
11 |
2 3 10
|
strfv |
|- ( x. e. _V -> x. = ( .r ` CCfld ) ) |
12 |
1 11
|
ax-mp |
|- x. = ( .r ` CCfld ) |