This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in GrpOp \to X \neq \emptyset$

Step	Hyp	Ref	Expression
1		grpfo.1	$⊢ X = ran G$
2	1	grpolidinv	$⊢ G \in GrpOp \to \exists u \in X \forall x \in X (u G x = x \land \exists y \in X y G x = u)$
3		rexn0	$⊢ \exists u \in X \forall x \in X (u G x = x \land \exists y \in X y G x = u) \to X \neq \emptyset$
4	2 3	syl	$⊢ G \in GrpOp \to X \neq \emptyset$