Step |
Hyp |
Ref |
Expression |
1 |
|
mnd1.m |
⊢ 𝑀 = { 〈 ( Base ‘ ndx ) , { 𝐼 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 〉 } |
2 |
1
|
sgrp1 |
⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Smgrp ) |
3 |
|
df-ov |
⊢ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = ( { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ‘ 〈 𝐼 , 𝐼 〉 ) |
4 |
|
opex |
⊢ 〈 𝐼 , 𝐼 〉 ∈ V |
5 |
|
fvsng |
⊢ ( ( 〈 𝐼 , 𝐼 〉 ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ‘ 〈 𝐼 , 𝐼 〉 ) = 𝐼 ) |
6 |
4 5
|
mpan |
⊢ ( 𝐼 ∈ 𝑉 → ( { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ‘ 〈 𝐼 , 𝐼 〉 ) = 𝐼 ) |
7 |
3 6
|
eqtrid |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ) |
8 |
|
oveq2 |
⊢ ( 𝑦 = 𝐼 → ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) |
9 |
|
id |
⊢ ( 𝑦 = 𝐼 → 𝑦 = 𝐼 ) |
10 |
8 9
|
eqeq12d |
⊢ ( 𝑦 = 𝐼 → ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ↔ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ) ) |
11 |
|
oveq1 |
⊢ ( 𝑦 = 𝐼 → ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) ) |
12 |
11 9
|
eqeq12d |
⊢ ( 𝑦 = 𝐼 → ( ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑦 ↔ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ) ) |
13 |
10 12
|
anbi12d |
⊢ ( 𝑦 = 𝐼 → ( ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ∧ ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑦 ) ↔ ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ∧ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ) ) ) |
14 |
13
|
ralsng |
⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑦 ∈ { 𝐼 } ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ∧ ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑦 ) ↔ ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ∧ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝐼 ) ) ) |
15 |
7 7 14
|
mpbir2and |
⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑦 ∈ { 𝐼 } ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ∧ ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑦 ) ) |
16 |
|
oveq1 |
⊢ ( 𝑥 = 𝐼 → ( 𝑥 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) ) |
17 |
16
|
eqeq1d |
⊢ ( 𝑥 = 𝐼 → ( ( 𝑥 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ↔ ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ) ) |
18 |
17
|
ovanraleqv |
⊢ ( 𝑥 = 𝐼 → ( ∀ 𝑦 ∈ { 𝐼 } ( ( 𝑥 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ∧ ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝐼 } ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ∧ ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑦 ) ) ) |
19 |
18
|
rexsng |
⊢ ( 𝐼 ∈ 𝑉 → ( ∃ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( ( 𝑥 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ∧ ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝐼 } ( ( 𝐼 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ∧ ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝐼 ) = 𝑦 ) ) ) |
20 |
15 19
|
mpbird |
⊢ ( 𝐼 ∈ 𝑉 → ∃ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( ( 𝑥 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ∧ ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑥 ) = 𝑦 ) ) |
21 |
|
snex |
⊢ { 𝐼 } ∈ V |
22 |
1
|
grpbase |
⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) ) |
23 |
21 22
|
ax-mp |
⊢ { 𝐼 } = ( Base ‘ 𝑀 ) |
24 |
|
snex |
⊢ { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ∈ V |
25 |
1
|
grpplusg |
⊢ ( { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } ∈ V → { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } = ( +g ‘ 𝑀 ) ) |
26 |
24 25
|
ax-mp |
⊢ { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } = ( +g ‘ 𝑀 ) |
27 |
23 26
|
ismnddef |
⊢ ( 𝑀 ∈ Mnd ↔ ( 𝑀 ∈ Smgrp ∧ ∃ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( ( 𝑥 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑦 ) = 𝑦 ∧ ( 𝑦 { 〈 〈 𝐼 , 𝐼 〉 , 𝐼 〉 } 𝑥 ) = 𝑦 ) ) ) |
28 |
2 20 27
|
sylanbrc |
⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd ) |