Description: The base set of a constructed two-slot structure. Version of 2strbas not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2str1.g | ⊢ 𝐺 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 𝑁 , + 〉 } | |
2str1.b | ⊢ ( Base ‘ ndx ) < 𝑁 | ||
2str1.n | ⊢ 𝑁 ∈ ℕ | ||
Assertion | 2strbas1 | ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐺 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2str1.g | ⊢ 𝐺 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 𝑁 , + 〉 } | |
2 | 2str1.b | ⊢ ( Base ‘ ndx ) < 𝑁 | |
3 | 2str1.n | ⊢ 𝑁 ∈ ℕ | |
4 | 1 2 3 | 2strstr1 | ⊢ 𝐺 Struct 〈 ( Base ‘ ndx ) , 𝑁 〉 |
5 | baseid | ⊢ Base = Slot ( Base ‘ ndx ) | |
6 | snsspr1 | ⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 } ⊆ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 𝑁 , + 〉 } | |
7 | 6 1 | sseqtrri | ⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 } ⊆ 𝐺 |
8 | 4 5 7 | strfv | ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐺 ) ) |