Theorem 0ngrp

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

	Ref	Expression
Assertion	0ngrp	⊢ ¬ ∅ ∈ GrpOp

Proof

Step	Hyp	Ref	Expression
1		neirr	⊢ ¬ ∅ ≠ ∅
2		rn0	⊢ ran ∅ = ∅
3	2	eqcomi	⊢ ∅ = ran ∅
4	3	grpon0	⊢ ( ∅ ∈ GrpOp → ∅ ≠ ∅ )
5	1 4	mto	⊢ ¬ ∅ ∈ GrpOp