Description: The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015) Use the index-independent version 2strop1 instead. (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2str.g | |- G = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. } |
|
2str.e | |- E = Slot N |
||
2str.l | |- 1 < N |
||
2str.n | |- N e. NN |
||
Assertion | 2strop | |- ( .+ e. V -> .+ = ( E ` G ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2str.g | |- G = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. } |
|
2 | 2str.e | |- E = Slot N |
|
3 | 2str.l | |- 1 < N |
|
4 | 2str.n | |- N e. NN |
|
5 | 1 2 3 4 | 2strstr | |- G Struct <. 1 , N >. |
6 | 2 4 | ndxid | |- E = Slot ( E ` ndx ) |
7 | snsspr2 | |- { <. ( E ` ndx ) , .+ >. } C_ { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. } |
|
8 | 7 1 | sseqtrri | |- { <. ( E ` ndx ) , .+ >. } C_ G |
9 | 5 6 8 | strfv | |- ( .+ e. V -> .+ = ( E ` G ) ) |