Step |
Hyp |
Ref |
Expression |
1 |
|
mnd1.m |
⊢ 𝑀 = { 〈 ( Base ‘ ndx ) , { 𝐼 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 〉 } |
2 |
|
snex |
⊢ { 𝐼 } ∈ V |
3 |
1
|
grpbase |
⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) ) |
4 |
2 3
|
ax-mp |
⊢ { 𝐼 } = ( Base ‘ 𝑀 ) |
5 |
|
eqid |
⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 ) |
6 |
|
snex |
⊢ { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ∈ V |
7 |
1
|
grpplusg |
⊢ ( { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ∈ V → { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } = ( +g ‘ 𝑀 ) ) |
8 |
6 7
|
ax-mp |
⊢ { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } = ( +g ‘ 𝑀 ) |
9 |
|
snidg |
⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } ) |
10 |
|
velsn |
⊢ ( 𝑎 ∈ { 𝐼 } ↔ 𝑎 = 𝐼 ) |
11 |
|
df-ov |
⊢ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = ( { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ‘ 〈 𝐼 , 𝐼 〉 ) |
12 |
|
opex |
⊢ 〈 𝐼 , 𝐼 〉 ∈ V |
13 |
|
fvsng |
⊢ ( ( 〈 𝐼 , 𝐼 〉 ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ‘ 〈 𝐼 , 𝐼 〉 ) = 𝐼 ) |
14 |
12 13
|
mpan |
⊢ ( 𝐼 ∈ 𝑉 → ( { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ‘ 〈 𝐼 , 𝐼 〉 ) = 𝐼 ) |
15 |
11 14
|
eqtrid |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ) |
16 |
|
oveq2 |
⊢ ( 𝑎 = 𝐼 → ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) |
17 |
|
id |
⊢ ( 𝑎 = 𝐼 → 𝑎 = 𝐼 ) |
18 |
16 17
|
eqeq12d |
⊢ ( 𝑎 = 𝐼 → ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) = 𝑎 ↔ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ) ) |
19 |
15 18
|
syl5ibrcom |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 = 𝐼 → ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) = 𝑎 ) ) |
20 |
10 19
|
syl5bi |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 ∈ { 𝐼 } → ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) = 𝑎 ) ) |
21 |
20
|
imp |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑎 ∈ { 𝐼 } ) → ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑎 ) = 𝑎 ) |
22 |
|
oveq1 |
⊢ ( 𝑎 = 𝐼 → ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) |
23 |
22 17
|
eqeq12d |
⊢ ( 𝑎 = 𝐼 → ( ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑎 ↔ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ) ) |
24 |
15 23
|
syl5ibrcom |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 = 𝐼 → ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑎 ) ) |
25 |
10 24
|
syl5bi |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 ∈ { 𝐼 } → ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑎 ) ) |
26 |
25
|
imp |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑎 ∈ { 𝐼 } ) → ( 𝑎 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑎 ) |
27 |
4 5 8 9 21 26
|
ismgmid2 |
⊢ ( 𝐼 ∈ 𝑉 → 𝐼 = ( 0g ‘ 𝑀 ) ) |
28 |
27
|
eqcomd |
⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝑀 ) = 𝐼 ) |