Metamath Proof Explorer

Theorem iorlid

Description: A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	iorlid.1	$⊢ X = ran G$
		iorlid.2	$⊢ U = GId (G)$
	Assertion	iorlid	$⊢ G \in (Magma \cap ExId) \to U \in X$

Proof

Step	Hyp	Ref	Expression
1		iorlid.1	$⊢ X = ran G$
2		iorlid.2	$⊢ U = GId (G)$
3	1 2	idrval	$⊢ G \in (Magma \cap ExId) \to U = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$
4	1	exidu1	$⊢ G \in (Magma \cap ExId) \to \exists! u \in X \forall x \in X (u G x = x \land x G u = x)$
5		riotacl	$⊢ \exists! u \in X \forall x \in X (u G x = x \land x G u = x) \to (ι u \in X \| \forall x \in X (u G x = x \land x G u = x)) \in X$
6	4 5	syl	$⊢ G \in (Magma \cap ExId) \to (ι u \in X \| \forall x \in X (u G x = x \land x G u = x)) \in X$
7	3 6	eqeltrd	$⊢ G \in (Magma \cap ExId) \to U \in X$