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

Metamath Proof Explorer

Theorem grpn0

Description: A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007) (Revised by Mario Carneiro, 2-Dec-2014)

		Ref	Expression
	Assertion	grpn0	$⊢ G \in Grp \to G \neq \emptyset$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{G} = {Base}_{G}$
2	1	grpbn0	$⊢ G \in Grp \to {Base}_{G} \neq \emptyset$
3		fveq2	$⊢ G = \emptyset \to {Base}_{G} = {Base}_{\emptyset}$
4		base0	$⊢ \emptyset = {Base}_{\emptyset}$
5	3 4	eqtr4di	$⊢ G = \emptyset \to {Base}_{G} = \emptyset$
6	5	necon3i	$⊢ {Base}_{G} \neq \emptyset \to G \neq \emptyset$
7	2 6	syl	$⊢ G \in Grp \to G \neq \emptyset$