| Step | Hyp | Ref
 | Expression | 
| 1 |   | grp1.m | 
. . 3
⊢ 𝑀 = {〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} | 
| 2 | 1 | mnd1 13087 | 
. 2
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) | 
| 3 |   | df-ov 5925 | 
. . . . 5
⊢ (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = ({〈〈𝐼, 𝐼〉, 𝐼〉}‘〈𝐼, 𝐼〉) | 
| 4 |   | opexg 4261 | 
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → 〈𝐼, 𝐼〉 ∈ V) | 
| 5 | 4 | anidms 397 | 
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → 〈𝐼, 𝐼〉 ∈ V) | 
| 6 |   | fvsng 5758 | 
. . . . . 6
⊢
((〈𝐼, 𝐼〉 ∈ V ∧ 𝐼 ∈ 𝑉) → ({〈〈𝐼, 𝐼〉, 𝐼〉}‘〈𝐼, 𝐼〉) = 𝐼) | 
| 7 | 5, 6 | mpancom 422 | 
. . . . 5
⊢ (𝐼 ∈ 𝑉 → ({〈〈𝐼, 𝐼〉, 𝐼〉}‘〈𝐼, 𝐼〉) = 𝐼) | 
| 8 | 3, 7 | eqtrid 2241 | 
. . . 4
⊢ (𝐼 ∈ 𝑉 → (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = 𝐼) | 
| 9 | 1 | mnd1id 13088 | 
. . . 4
⊢ (𝐼 ∈ 𝑉 → (0g‘𝑀) = 𝐼) | 
| 10 | 8, 9 | eqtr4d 2232 | 
. . 3
⊢ (𝐼 ∈ 𝑉 → (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (0g‘𝑀)) | 
| 11 |   | oveq2 5930 | 
. . . . . . 7
⊢ (𝑖 = 𝐼 → (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)) | 
| 12 | 11 | eqeq1d 2205 | 
. . . . . 6
⊢ (𝑖 = 𝐼 → ((𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀) ↔ (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (0g‘𝑀))) | 
| 13 | 12 | rexbidv 2498 | 
. . . . 5
⊢ (𝑖 = 𝐼 → (∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀) ↔ ∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (0g‘𝑀))) | 
| 14 | 13 | ralsng 3662 | 
. . . 4
⊢ (𝐼 ∈ 𝑉 → (∀𝑖 ∈ {𝐼}∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀) ↔ ∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (0g‘𝑀))) | 
| 15 |   | oveq1 5929 | 
. . . . . 6
⊢ (𝑒 = 𝐼 → (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)) | 
| 16 | 15 | eqeq1d 2205 | 
. . . . 5
⊢ (𝑒 = 𝐼 → ((𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (0g‘𝑀) ↔ (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (0g‘𝑀))) | 
| 17 | 16 | rexsng 3663 | 
. . . 4
⊢ (𝐼 ∈ 𝑉 → (∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (0g‘𝑀) ↔ (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (0g‘𝑀))) | 
| 18 | 14, 17 | bitrd 188 | 
. . 3
⊢ (𝐼 ∈ 𝑉 → (∀𝑖 ∈ {𝐼}∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀) ↔ (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (0g‘𝑀))) | 
| 19 | 10, 18 | mpbird 167 | 
. 2
⊢ (𝐼 ∈ 𝑉 → ∀𝑖 ∈ {𝐼}∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀)) | 
| 20 |   | eqid 2196 | 
. . . 4
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 21 |   | eqid 2196 | 
. . . 4
⊢
(+g‘𝑀) = (+g‘𝑀) | 
| 22 |   | eqid 2196 | 
. . . 4
⊢
(0g‘𝑀) = (0g‘𝑀) | 
| 23 | 20, 21, 22 | isgrp 13138 | 
. . 3
⊢ (𝑀 ∈ Grp ↔ (𝑀 ∈ Mnd ∧ ∀𝑖 ∈ (Base‘𝑀)∃𝑒 ∈ (Base‘𝑀)(𝑒(+g‘𝑀)𝑖) = (0g‘𝑀))) | 
| 24 |   | snexg 4217 | 
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → {𝐼} ∈ V) | 
| 25 |   | opexg 4261 | 
. . . . . . . 8
⊢
((〈𝐼, 𝐼〉 ∈ V ∧ 𝐼 ∈ 𝑉) → 〈〈𝐼, 𝐼〉, 𝐼〉 ∈ V) | 
| 26 | 5, 25 | mpancom 422 | 
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → 〈〈𝐼, 𝐼〉, 𝐼〉 ∈ V) | 
| 27 |   | snexg 4217 | 
. . . . . . 7
⊢
(〈〈𝐼,
𝐼〉, 𝐼〉 ∈ V → {〈〈𝐼, 𝐼〉, 𝐼〉} ∈ V) | 
| 28 | 26, 27 | syl 14 | 
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → {〈〈𝐼, 𝐼〉, 𝐼〉} ∈ V) | 
| 29 | 1 | grpbaseg 12804 | 
. . . . . 6
⊢ (({𝐼} ∈ V ∧
{〈〈𝐼, 𝐼〉, 𝐼〉} ∈ V) → {𝐼} = (Base‘𝑀)) | 
| 30 | 24, 28, 29 | syl2anc 411 | 
. . . . 5
⊢ (𝐼 ∈ 𝑉 → {𝐼} = (Base‘𝑀)) | 
| 31 | 1 | grpplusgg 12805 | 
. . . . . . . . 9
⊢ (({𝐼} ∈ V ∧
{〈〈𝐼, 𝐼〉, 𝐼〉} ∈ V) → {〈〈𝐼, 𝐼〉, 𝐼〉} = (+g‘𝑀)) | 
| 32 | 24, 28, 31 | syl2anc 411 | 
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → {〈〈𝐼, 𝐼〉, 𝐼〉} = (+g‘𝑀)) | 
| 33 | 32 | oveqd 5939 | 
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (𝑒(+g‘𝑀)𝑖)) | 
| 34 | 33 | eqeq1d 2205 | 
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → ((𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀) ↔ (𝑒(+g‘𝑀)𝑖) = (0g‘𝑀))) | 
| 35 | 30, 34 | rexeqbidv 2710 | 
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀) ↔ ∃𝑒 ∈ (Base‘𝑀)(𝑒(+g‘𝑀)𝑖) = (0g‘𝑀))) | 
| 36 | 30, 35 | raleqbidv 2709 | 
. . . 4
⊢ (𝐼 ∈ 𝑉 → (∀𝑖 ∈ {𝐼}∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀) ↔ ∀𝑖 ∈ (Base‘𝑀)∃𝑒 ∈ (Base‘𝑀)(𝑒(+g‘𝑀)𝑖) = (0g‘𝑀))) | 
| 37 | 36 | anbi2d 464 | 
. . 3
⊢ (𝐼 ∈ 𝑉 → ((𝑀 ∈ Mnd ∧ ∀𝑖 ∈ {𝐼}∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀)) ↔ (𝑀 ∈ Mnd ∧ ∀𝑖 ∈ (Base‘𝑀)∃𝑒 ∈ (Base‘𝑀)(𝑒(+g‘𝑀)𝑖) = (0g‘𝑀)))) | 
| 38 | 23, 37 | bitr4id 199 | 
. 2
⊢ (𝐼 ∈ 𝑉 → (𝑀 ∈ Grp ↔ (𝑀 ∈ Mnd ∧ ∀𝑖 ∈ {𝐼}∃𝑒 ∈ {𝐼} (𝑒{〈〈𝐼, 𝐼〉, 𝐼〉}𝑖) = (0g‘𝑀)))) | 
| 39 | 2, 19, 38 | mpbir2and 946 | 
1
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Grp) |