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