Metamath Proof Explorer

Theorem grpoidcl

Description: The identity element of a group belongs to the group. (Contributed by NM, 24-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	grpoidval.1	$⊢ X = ran G$
		grpoidval.2	$⊢ U = GId (G)$
	Assertion	grpoidcl	$⊢ G \in GrpOp \to U \in X$

Proof

Step	Hyp	Ref	Expression
1		grpoidval.1	$⊢ X = ran G$
2		grpoidval.2	$⊢ U = GId (G)$
3	1 2	grpoidval	$⊢ G \in GrpOp \to U = (ι u \in X \| \forall x \in X u G x = x)$
4	1	grpoideu	$⊢ G \in GrpOp \to \exists! u \in X \forall x \in X u G x = x$
5		riotacl	$⊢ \exists! u \in X \forall x \in X u G x = x \to (ι u \in X \| \forall x \in X u G x = x) \in X$
6	4 5	syl	$⊢ G \in GrpOp \to (ι u \in X \| \forall x \in X u G x = x) \in X$
7	3 6	eqeltrd	$⊢ G \in GrpOp \to U \in X$