Metamath Proof Explorer

Theorem subgid

Description: A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypothesis issubg.b ⊢ B = Base G
Assertion subgid ⊢ G ∈ Grp → B ∈ SubGrp ⁡ G

Proof

Step Hyp Ref Expression
1 issubg.b ⊢ B = Base G
2 id ⊢ G ∈ Grp → G ∈ Grp
3 ssidd ⊢ G ∈ Grp → B ⊆ B
4 1 ressid ⊢ G ∈ Grp → G ↾ 𝑠 B = G
5 4 2 eqeltrd ⊢ G ∈ Grp → G ↾ 𝑠 B ∈ Grp
6 1 issubg ⊢ B ∈ SubGrp ⁡ G ↔ G ∈ Grp ∧ B ⊆ B ∧ G ↾ 𝑠 B ∈ Grp
7 2 3 5 6 syl3anbrc ⊢ G ∈ Grp → B ∈ SubGrp ⁡ G