Description: The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013) (Revised by Mario Carneiro, 30-Apr-2015) (Revised by AV, 27-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | grpfn.g | |- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } |
|
| Assertion | grpbase | |- ( B e. V -> B = ( Base ` G ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpfn.g | |- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } |
|
| 2 | basendxltplusgndx | |- ( Base ` ndx ) < ( +g ` ndx ) |
|
| 3 | plusgndxnn | |- ( +g ` ndx ) e. NN |
|
| 4 | 1 2 3 | 2strbas | |- ( B e. V -> B = ( Base ` G ) ) |