Description: The identity element of a group belongs to the group. (Contributed by NM, 24-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | grpoidval.1 | ⊢ 𝑋 = ran 𝐺 | |
| grpoidval.2 | ⊢ 𝑈 = ( GId ‘ 𝐺 ) | ||
| Assertion | grpoidcl | ⊢ ( 𝐺 ∈ GrpOp → 𝑈 ∈ 𝑋 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpoidval.1 | ⊢ 𝑋 = ran 𝐺 | |
| 2 | grpoidval.2 | ⊢ 𝑈 = ( GId ‘ 𝐺 ) | |
| 3 | 1 2 | grpoidval | ⊢ ( 𝐺 ∈ GrpOp → 𝑈 = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ) |
| 4 | 1 | grpoideu | ⊢ ( 𝐺 ∈ GrpOp → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) |
| 5 | riotacl | ⊢ ( ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 → ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∈ 𝑋 ) | |
| 6 | 4 5 | syl | ⊢ ( 𝐺 ∈ GrpOp → ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∈ 𝑋 ) |
| 7 | 3 6 | eqeltrd | ⊢ ( 𝐺 ∈ GrpOp → 𝑈 ∈ 𝑋 ) |