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 ˙ = 0 G
Assertion 0subgALT ⊢ G ∈ Grp → 0 ˙ ∈ SubGrp ⁡ G

Proof

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