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=\mathrm{ran}G$$
Assertion	grpon0	$$⊢G\in \mathrm{GrpOp}\to X\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	$$⊢X=\mathrm{ran}G$$
2	1	grpolidinv	$$⊢G\in \mathrm{GrpOp}\to \exists u\in X\forall x\in X\left(uGx=x\wedge \exists y\in XyGx=u\right)$$
3		rexn0	$$⊢\exists u\in X\forall x\in X\left(uGx=x\wedge \exists y\in XyGx=u\right)\to X\ne \varnothing$$
4	2 3	syl	$$⊢G\in \mathrm{GrpOp}\to X\ne \varnothing$$