| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prhash2ex 14438 | . 2
⊢
(♯‘{0, 1}) = 2 | 
| 2 |  | c0ex 11255 | . . . . 5
⊢ 0 ∈
V | 
| 3 |  | 1ex 11257 | . . . . 5
⊢ 1 ∈
V | 
| 4 | 2, 3 | pm3.2i 470 | . . . 4
⊢ (0 ∈
V ∧ 1 ∈ V) | 
| 5 |  | eqid 2737 | . . . . 5
⊢ {0, 1} =
{0, 1} | 
| 6 |  | prex 5437 | . . . . . . 7
⊢ {0, 1}
∈ V | 
| 7 |  | eqeq1 2741 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑢 → (𝑥 = 0 ↔ 𝑢 = 0)) | 
| 8 | 7 | anbi1d 631 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → ((𝑥 = 0 ∧ 𝑦 = 0) ↔ (𝑢 = 0 ∧ 𝑦 = 0))) | 
| 9 | 8 | ifbid 4549 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0) = if((𝑢 = 0 ∧ 𝑦 = 0), 1, 0)) | 
| 10 |  | eqeq1 2741 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → (𝑦 = 0 ↔ 𝑣 = 0)) | 
| 11 | 10 | anbi2d 630 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑣 → ((𝑢 = 0 ∧ 𝑦 = 0) ↔ (𝑢 = 0 ∧ 𝑣 = 0))) | 
| 12 | 11 | ifbid 4549 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑣 → if((𝑢 = 0 ∧ 𝑦 = 0), 1, 0) = if((𝑢 = 0 ∧ 𝑣 = 0), 1, 0)) | 
| 13 | 9, 12 | cbvmpov 7528 | . . . . . . . . . 10
⊢ (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0)) = (𝑢 ∈ {0, 1}, 𝑣 ∈ {0, 1} ↦ if((𝑢 = 0 ∧ 𝑣 = 0), 1, 0)) | 
| 14 | 13 | opeq2i 4877 | . . . . . . . . 9
⊢
〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉 =
〈(+g‘ndx), (𝑢 ∈ {0, 1}, 𝑣 ∈ {0, 1} ↦ if((𝑢 = 0 ∧ 𝑣 = 0), 1, 0))〉 | 
| 15 | 14 | preq2i 4737 | . . . . . . . 8
⊢
{〈(Base‘ndx), {0, 1}〉, 〈(+g‘ndx),
(𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉} =
{〈(Base‘ndx), {0, 1}〉, 〈(+g‘ndx), (𝑢 ∈ {0, 1}, 𝑣 ∈ {0, 1} ↦ if((𝑢 = 0 ∧ 𝑣 = 0), 1, 0))〉} | 
| 16 | 15 | grpbase 17330 | . . . . . . 7
⊢ ({0, 1}
∈ V → {0, 1} = (Base‘{〈(Base‘ndx), {0, 1}〉,
〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉})) | 
| 17 | 6, 16 | ax-mp 5 | . . . . . 6
⊢ {0, 1} =
(Base‘{〈(Base‘ndx), {0, 1}〉,
〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉}) | 
| 18 | 17 | eqcomi 2746 | . . . . 5
⊢
(Base‘{〈(Base‘ndx), {0, 1}〉,
〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉}) = {0,
1} | 
| 19 | 6, 6 | mpoex 8104 | . . . . . . 7
⊢ (𝑢 ∈ {0, 1}, 𝑣 ∈ {0, 1} ↦ if((𝑢 = 0 ∧ 𝑣 = 0), 1, 0)) ∈ V | 
| 20 | 15 | grpplusg 17332 | . . . . . . 7
⊢ ((𝑢 ∈ {0, 1}, 𝑣 ∈ {0, 1} ↦ if((𝑢 = 0 ∧ 𝑣 = 0), 1, 0)) ∈ V → (𝑢 ∈ {0, 1}, 𝑣 ∈ {0, 1} ↦ if((𝑢 = 0 ∧ 𝑣 = 0), 1, 0)) =
(+g‘{〈(Base‘ndx), {0, 1}〉,
〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉})) | 
| 21 | 19, 20 | ax-mp 5 | . . . . . 6
⊢ (𝑢 ∈ {0, 1}, 𝑣 ∈ {0, 1} ↦ if((𝑢 = 0 ∧ 𝑣 = 0), 1, 0)) =
(+g‘{〈(Base‘ndx), {0, 1}〉,
〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉}) | 
| 22 | 21 | eqcomi 2746 | . . . . 5
⊢
(+g‘{〈(Base‘ndx), {0, 1}〉,
〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉}) = (𝑢 ∈ {0, 1}, 𝑣 ∈ {0, 1} ↦ if((𝑢 = 0 ∧ 𝑣 = 0), 1, 0)) | 
| 23 | 5, 18, 22 | mgm2nsgrplem1 18931 | . . . 4
⊢ ((0
∈ V ∧ 1 ∈ V) → {〈(Base‘ndx), {0, 1}〉,
〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉} ∈
Mgm) | 
| 24 | 4, 23 | mp1i 13 | . . 3
⊢
((♯‘{0, 1}) = 2 → {〈(Base‘ndx), {0,
1}〉, 〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉} ∈
Mgm) | 
| 25 |  | neleq1 3052 | . . . 4
⊢ (𝑚 = {〈(Base‘ndx), {0,
1}〉, 〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉} → (𝑚 ∉ Smgrp ↔
{〈(Base‘ndx), {0, 1}〉, 〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉} ∉
Smgrp)) | 
| 26 | 25 | adantl 481 | . . 3
⊢
(((♯‘{0, 1}) = 2 ∧ 𝑚 = {〈(Base‘ndx), {0, 1}〉,
〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉}) → (𝑚 ∉ Smgrp ↔
{〈(Base‘ndx), {0, 1}〉, 〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉} ∉
Smgrp)) | 
| 27 | 5, 18, 22 | mgm2nsgrplem4 18934 | . . 3
⊢
((♯‘{0, 1}) = 2 → {〈(Base‘ndx), {0,
1}〉, 〈(+g‘ndx), (𝑥 ∈ {0, 1}, 𝑦 ∈ {0, 1} ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 1, 0))〉} ∉
Smgrp) | 
| 28 | 24, 26, 27 | rspcedvd 3624 | . 2
⊢
((♯‘{0, 1}) = 2 → ∃𝑚 ∈ Mgm 𝑚 ∉ Smgrp) | 
| 29 | 1, 28 | ax-mp 5 | 1
⊢
∃𝑚 ∈ Mgm
𝑚 ∉
Smgrp |