Theorem idrval

Description: The value of the identity element. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	idrval.1	$$⊢X=\mathrm{ran}G$$
	idrval.2	$$⊢U=\mathrm{GId}\left(G\right)$$
Assertion	idrval	$$⊢G\in A\to U=\left(\iota u\in X|\forall x\in X\left(uGx=x\wedge xGu=x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		idrval.1	$$⊢X=\mathrm{ran}G$$
2		idrval.2	$$⊢U=\mathrm{GId}\left(G\right)$$
3	1	gidval	$$⊢G\in A\to \mathrm{GId}\left(G\right)=\left(\iota u\in X|\forall x\in X\left(uGx=x\wedge xGu=x\right)\right)$$
4	2 3	syl5eq	$$⊢G\in A\to U=\left(\iota u\in X|\forall x\in X\left(uGx=x\wedge xGu=x\right)\right)$$