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 e. GrpOp -> X =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	|- X = ran G
2	1	grpolidinv	|- ( G e. GrpOp -> E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) )
3		rexn0	|- ( E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) -> X =/= (/) )
4	2 3	syl	|- ( G e. GrpOp -> X =/= (/) )