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 \varnothing \in \mathrm{GrpOp}$$

Proof

Step	Hyp	Ref	Expression
1		neirr	$$⊢\neg \varnothing \ne \varnothing$$
2		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
3	2	eqcomi	$$⊢\varnothing =\mathrm{ran}\varnothing$$
4	3	grpon0	$$⊢\varnothing \in \mathrm{GrpOp}\to \varnothing \ne \varnothing$$
5	1 4	mto	$$⊢\neg \varnothing \in \mathrm{GrpOp}$$