Description: The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 1str.g | |- G = { <. ( Base ` ndx ) , B >. } |
|
Assertion | 1strbas | |- ( B e. V -> B = ( Base ` G ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1str.g | |- G = { <. ( Base ` ndx ) , B >. } |
|
2 | 1 | 1strstr | |- G Struct <. 1 , 1 >. |
3 | baseid | |- Base = Slot ( Base ` ndx ) |
|
4 | 1 | eqimss2i | |- { <. ( Base ` ndx ) , B >. } C_ G |
5 | 2 3 4 | strfv | |- ( B e. V -> B = ( Base ` G ) ) |