Description: Obsolete version of grpbase as of 27-Oct-2024. The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013) (Revised by Mario Carneiro, 30-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | grpfn.g | |- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } |
|
| Assertion | grpbaseOLD | |- ( B e. V -> B = ( Base ` G ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpfn.g | |- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } |
|
| 2 | df-plusg | |- +g = Slot 2 |
|
| 3 | 1lt2 | |- 1 < 2 |
|
| 4 | 2nn | |- 2 e. NN |
|
| 5 | 1 2 3 4 | 2strbas | |- ( B e. V -> B = ( Base ` G ) ) |