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	⊢ 𝑋 = ran 𝐺
	iorlid.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
Assertion	iorlid	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝑈 ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		iorlid.1	⊢ 𝑋 = ran 𝐺
2		iorlid.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
3	1 2	idrval	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝑈 = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
4	1	exidu1	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
5		riotacl	⊢ ( ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ∈ 𝑋 )
6	4 5	syl	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ∈ 𝑋 )
7	3 6	eqeltrd	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝑈 ∈ 𝑋 )