Metamath Proof Explorer

Theorem grpon0

Description: The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 X = ran G
Assertion grpon0 G GrpOp X


Step Hyp Ref Expression
1 grpfo.1 X = ran G
2 1 grpolidinv G GrpOp u X x X u G x = x y X y G x = u
3 rexn0 u X x X u G x = x y X y G x = u X
4 2 3 syl G GrpOp X