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