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	⊢ 𝑋 = ran 𝐺
	idrval.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
Assertion	idrval	⊢ ( 𝐺 ∈ 𝐴 → 𝑈 = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		idrval.1	⊢ 𝑋 = ran 𝐺
2		idrval.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
3	1	gidval	⊢ ( 𝐺 ∈ 𝐴 → ( GId ‘ 𝐺 ) = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
4	2 3	syl5eq	⊢ ( 𝐺 ∈ 𝐴 → 𝑈 = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )