Metamath Proof Explorer


Theorem grpbase

Description: The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypothesis grpfn.g
|- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }
Assertion grpbase
|- ( B e. V -> B = ( Base ` G ) )

Proof

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 ) )