Metamath Proof Explorer


Theorem 2strstr

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

Proof

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