Description: The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015) Use the index-independent version 2strbas1 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 | 2strbas | |- ( B e. V -> B = ( Base ` 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 | baseid | |- Base = Slot ( Base ` ndx ) |
|
7 | snsspr1 | |- { <. ( Base ` ndx ) , B >. } C_ { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. } |
|
8 | 7 1 | sseqtrri | |- { <. ( Base ` ndx ) , B >. } C_ G |
9 | 5 6 8 | strfv | |- ( B e. V -> B = ( Base ` G ) ) |