Metamath Proof Explorer


Theorem 2strstr1

Description: A constructed two-slot structure. Version of 2strstr not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020) (Proof shortened by AV, 17-Oct-2024)

Ref Expression
Hypotheses 2str1.g 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ 𝑁 , + ⟩ }
2str1.b ( Base ‘ ndx ) < 𝑁
2str1.n 𝑁 ∈ ℕ
Assertion 2strstr1 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑁

Proof

Step Hyp Ref Expression
1 2str1.g 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ 𝑁 , + ⟩ }
2 2str1.b ( Base ‘ ndx ) < 𝑁
3 2str1.n 𝑁 ∈ ℕ
4 basendxnn ( Base ‘ ndx ) ∈ ℕ
5 eqid ( Base ‘ ndx ) = ( Base ‘ ndx )
6 eqid 𝑁 = 𝑁
7 4 5 2 3 6 strle2 { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ 𝑁 , + ⟩ } Struct ⟨ ( Base ‘ ndx ) , 𝑁
8 1 7 eqbrtri 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑁