Step |
Hyp |
Ref |
Expression |
1 |
|
2str1.g |
⊢ 𝐺 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 𝑁 , + 〉 } |
2 |
|
2str1.b |
⊢ ( Base ‘ ndx ) < 𝑁 |
3 |
|
2str1.n |
⊢ 𝑁 ∈ ℕ |
4 |
|
eqid |
⊢ Slot 𝑁 = Slot 𝑁 |
5 |
4 3
|
ndxarg |
⊢ ( Slot 𝑁 ‘ ndx ) = 𝑁 |
6 |
5
|
eqcomi |
⊢ 𝑁 = ( Slot 𝑁 ‘ ndx ) |
7 |
6
|
opeq1i |
⊢ 〈 𝑁 , + 〉 = 〈 ( Slot 𝑁 ‘ ndx ) , + 〉 |
8 |
7
|
preq2i |
⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 𝑁 , + 〉 } = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Slot 𝑁 ‘ ndx ) , + 〉 } |
9 |
1 8
|
eqtri |
⊢ 𝐺 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( Slot 𝑁 ‘ ndx ) , + 〉 } |
10 |
|
basendx |
⊢ ( Base ‘ ndx ) = 1 |
11 |
10 2
|
eqbrtrri |
⊢ 1 < 𝑁 |
12 |
9 4 11 3
|
2strstr |
⊢ 𝐺 Struct 〈 1 , 𝑁 〉 |
13 |
10
|
opeq1i |
⊢ 〈 ( Base ‘ ndx ) , 𝑁 〉 = 〈 1 , 𝑁 〉 |
14 |
12 13
|
breqtrri |
⊢ 𝐺 Struct 〈 ( Base ‘ ndx ) , 𝑁 〉 |