Theorem 0subgALT

Description: A shorter proof of 0subg using df-od . (Contributed by SN, 31-Jan-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	0subgALT.z	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	0subgALT	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		0subgALT.z	⊢ 0 = ( 0g ‘ 𝐺 )
2		eqid	⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
3		id	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Grp )
4		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
5	1	0subm	⊢ ( 𝐺 ∈ Mnd → { 0 } ∈ ( SubMnd ‘ 𝐺 ) )
6	4 5	syl	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubMnd ‘ 𝐺 ) )
7	2 1	od1	⊢ ( 𝐺 ∈ Grp → ( ( od ‘ 𝐺 ) ‘ 0 ) = 1 )
8		1nn	⊢ 1 ∈ ℕ
9	7 8	eqeltrdi	⊢ ( 𝐺 ∈ Grp → ( ( od ‘ 𝐺 ) ‘ 0 ) ∈ ℕ )
10	1	fvexi	⊢ 0 ∈ V
11		fveq2	⊢ ( 𝑎 = 0 → ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = ( ( od ‘ 𝐺 ) ‘ 0 ) )
12	11	eleq1d	⊢ ( 𝑎 = 0 → ( ( ( od ‘ 𝐺 ) ‘ 𝑎 ) ∈ ℕ ↔ ( ( od ‘ 𝐺 ) ‘ 0 ) ∈ ℕ ) )
13	10 12	ralsn	⊢ ( ∀ 𝑎 ∈ { 0 } ( ( od ‘ 𝐺 ) ‘ 𝑎 ) ∈ ℕ ↔ ( ( od ‘ 𝐺 ) ‘ 0 ) ∈ ℕ )
14	9 13	sylibr	⊢ ( 𝐺 ∈ Grp → ∀ 𝑎 ∈ { 0 } ( ( od ‘ 𝐺 ) ‘ 𝑎 ) ∈ ℕ )
15	2 3 6 14	finodsubmsubg	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )