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)

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 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 ) , 𝑁