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