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