Step |
Hyp |
Ref |
Expression |
1 |
|
srngstr.r |
|- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } ) |
2 |
1
|
srngstr |
|- R Struct <. 1 , 4 >. |
3 |
|
baseid |
|- Base = Slot ( Base ` ndx ) |
4 |
|
snsstp1 |
|- { <. ( Base ` ndx ) , B >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } |
5 |
|
ssun1 |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } ) |
6 |
5 1
|
sseqtrri |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } C_ R |
7 |
4 6
|
sstri |
|- { <. ( Base ` ndx ) , B >. } C_ R |
8 |
2 3 7
|
strfv |
|- ( B e. X -> B = ( Base ` R ) ) |