This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐺 ) )