Metamath Proof Explorer

Theorem iorlid

Description: Obsolete theorem, use mgmidcl instead. 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.) (Proof modification is discouraged.)

Ref Expression
Hypotheses iorlid.1 ⊢ X = ran ⁡ G
iorlid.2 ⊢ U = GId ⁡ G
Assertion iorlid ⊢ G ∈ Magma ∩ ExId → U ∈ X

Proof

Step Hyp Ref Expression
1 iorlid.1 ⊢ X = ran ⁡ G
2 iorlid.2 ⊢ U = GId ⁡ G
3 1 2 idrval ⊢ G ∈ Magma ∩ ExId → U = ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x
4 1 exidu1 ⊢ G ∈ Magma ∩ ExId → ∃! u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x
5 riotacl ⊢ ∃! u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x ∈ X
6 4 5 syl ⊢ G ∈ Magma ∩ ExId → ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x ∈ X
7 3 6 eqeltrd ⊢ G ∈ Magma ∩ ExId → U ∈ X