Theorem subgid

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

	Ref	Expression
Hypothesis	issubg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	subgid	⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		issubg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		id	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Grp )
3		ssidd	⊢ ( 𝐺 ∈ Grp → 𝐵 ⊆ 𝐵 )
4	1	ressid	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ↾s 𝐵 ) = 𝐺 )
5	4 2	eqeltrd	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ↾s 𝐵 ) ∈ Grp )
6	1	issubg	⊢ ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝐵 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝐵 ) ∈ Grp ) )
7	2 3 5 6	syl3anbrc	⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )