Description: The base set of a constructed two-slot structure. Version of 2strbas not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2str1.g | |- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. } |
|
2str1.b | |- ( Base ` ndx ) < N |
||
2str1.n | |- N e. NN |
||
Assertion | 2strbas1 | |- ( B e. V -> B = ( Base ` G ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2str1.g | |- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. } |
|
2 | 2str1.b | |- ( Base ` ndx ) < N |
|
3 | 2str1.n | |- N e. NN |
|
4 | 1 2 3 | 2strstr1 | |- G Struct <. ( Base ` ndx ) , N >. |
5 | baseid | |- Base = Slot ( Base ` ndx ) |
|
6 | snsspr1 | |- { <. ( Base ` ndx ) , B >. } C_ { <. ( Base ` ndx ) , B >. , <. N , .+ >. } |
|
7 | 6 1 | sseqtrri | |- { <. ( Base ` ndx ) , B >. } C_ G |
8 | 4 5 7 | strfv | |- ( B e. V -> B = ( Base ` G ) ) |