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

Metamath Proof Explorer

Theorem 0ngrp

Description: The empty set is not a group. (Contributed by NM, 25-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	0ngrp	$⊢ \neg \emptyset \in GrpOp$

Step	Hyp	Ref	Expression
1		neirr	$⊢ \neg \emptyset \neq \emptyset$
2		rn0	$⊢ ran \emptyset = \emptyset$
3	2	eqcomi	$⊢ \emptyset = ran \emptyset$
4	3	grpon0	$⊢ \emptyset \in GrpOp \to \emptyset \neq \emptyset$
5	1 4	mto	$⊢ \neg \emptyset \in GrpOp$