Step |
Hyp |
Ref |
Expression |
1 |
|
odrngstr.w |
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) |
2 |
1
|
odrngstr |
|- W Struct <. 1 , ; 1 2 >. |
3 |
|
pleid |
|- le = Slot ( le ` ndx ) |
4 |
|
snsstp2 |
|- { <. ( le ` ndx ) , .<_ >. } C_ { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } |
5 |
|
ssun2 |
|- { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) |
6 |
5 1
|
sseqtrri |
|- { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } C_ W |
7 |
4 6
|
sstri |
|- { <. ( le ` ndx ) , .<_ >. } C_ W |
8 |
2 3 7
|
strfv |
|- ( .<_ e. V -> .<_ = ( le ` W ) ) |