Description: The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020) (Proof shortened by AV, 15-Nov-2024)
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 | 1strstr1 | |- G Struct <. ( Base ` ndx ) , ( Base ` ndx ) >. |
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 ) ) |