Description: A constructed two-slot structure. Depending on hard-coded indices. Use 2strstr1 instead. (Contributed by Mario Carneiro, 29-Aug-2015) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2str.g | ⊢ 𝐺 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( 𝐸 ‘ ndx ) , + 〉 } | |
2str.e | ⊢ 𝐸 = Slot 𝑁 | ||
2str.l | ⊢ 1 < 𝑁 | ||
2str.n | ⊢ 𝑁 ∈ ℕ | ||
Assertion | 2strstr | ⊢ 𝐺 Struct 〈 1 , 𝑁 〉 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2str.g | ⊢ 𝐺 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( 𝐸 ‘ ndx ) , + 〉 } | |
2 | 2str.e | ⊢ 𝐸 = Slot 𝑁 | |
3 | 2str.l | ⊢ 1 < 𝑁 | |
4 | 2str.n | ⊢ 𝑁 ∈ ℕ | |
5 | 1nn | ⊢ 1 ∈ ℕ | |
6 | basendx | ⊢ ( Base ‘ ndx ) = 1 | |
7 | 2 4 | ndxarg | ⊢ ( 𝐸 ‘ ndx ) = 𝑁 |
8 | 5 6 3 4 7 | strle2 | ⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( 𝐸 ‘ ndx ) , + 〉 } Struct 〈 1 , 𝑁 〉 |
9 | 1 8 | eqbrtri | ⊢ 𝐺 Struct 〈 1 , 𝑁 〉 |