Step |
Hyp |
Ref |
Expression |
1 |
|
prhash2ex |
⊢ ( ♯ ‘ { 0 , 1 } ) = 2 |
2 |
|
eqid |
⊢ { 0 , 1 } = { 0 , 1 } |
3 |
|
prex |
⊢ { 0 , 1 } ∈ V |
4 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑢 → ( 𝑥 = 0 ↔ 𝑢 = 0 ) ) |
5 |
4
|
ifbid |
⊢ ( 𝑥 = 𝑢 → if ( 𝑥 = 0 , 0 , 1 ) = if ( 𝑢 = 0 , 0 , 1 ) ) |
6 |
|
eqidd |
⊢ ( 𝑦 = 𝑣 → if ( 𝑢 = 0 , 0 , 1 ) = if ( 𝑢 = 0 , 0 , 1 ) ) |
7 |
5 6
|
cbvmpov |
⊢ ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) = ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) |
8 |
7
|
opeq2i |
⊢ 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 = 〈 ( +g ‘ ndx ) , ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) 〉 |
9 |
8
|
preq2i |
⊢ { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } = { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) 〉 } |
10 |
9
|
grpbase |
⊢ ( { 0 , 1 } ∈ V → { 0 , 1 } = ( Base ‘ { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ) ) |
11 |
3 10
|
ax-mp |
⊢ { 0 , 1 } = ( Base ‘ { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ) |
12 |
11
|
eqcomi |
⊢ ( Base ‘ { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ) = { 0 , 1 } |
13 |
3 3
|
mpoex |
⊢ ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) ∈ V |
14 |
9
|
grpplusg |
⊢ ( ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) ∈ V → ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) = ( +g ‘ { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ) ) |
15 |
13 14
|
ax-mp |
⊢ ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) = ( +g ‘ { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ) |
16 |
15
|
eqcomi |
⊢ ( +g ‘ { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ) = ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) |
17 |
2 12 16
|
sgrp2nmndlem4 |
⊢ ( ( ♯ ‘ { 0 , 1 } ) = 2 → { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ∈ Smgrp ) |
18 |
|
neleq1 |
⊢ ( 𝑚 = { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } → ( 𝑚 ∉ Mnd ↔ { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ∉ Mnd ) ) |
19 |
18
|
adantl |
⊢ ( ( ( ♯ ‘ { 0 , 1 } ) = 2 ∧ 𝑚 = { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ) → ( 𝑚 ∉ Mnd ↔ { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ∉ Mnd ) ) |
20 |
2 12 16
|
sgrp2nmndlem5 |
⊢ ( ( ♯ ‘ { 0 , 1 } ) = 2 → { 〈 ( Base ‘ ndx ) , { 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) 〉 } ∉ Mnd ) |
21 |
17 19 20
|
rspcedvd |
⊢ ( ( ♯ ‘ { 0 , 1 } ) = 2 → ∃ 𝑚 ∈ Smgrp 𝑚 ∉ Mnd ) |
22 |
1 21
|
ax-mp |
⊢ ∃ 𝑚 ∈ Smgrp 𝑚 ∉ Mnd |