Metamath Proof Explorer


Theorem 2strbas1

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 ‘ 𝐺 ) )

Proof

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 ‘ 𝐺 ) )