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	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}$$
	2str1.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<N$$
	2str1.n	$$⊢N\in \mathbb{N}$$
Assertion	2strstr1	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},N⟩$$

Proof

Step	Hyp	Ref	Expression
1		2str1.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}$$
2		2str1.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<N$$
3		2str1.n	$$⊢N\in \mathbb{N}$$
4		eqid	$$⊢\mathrm{Slot}N=\mathrm{Slot}N$$
5	4 3	ndxarg	$$⊢\mathrm{Slot}N\left(\mathrm{ndx}\right)=N$$
6	5	eqcomi	$$⊢N=\mathrm{Slot}N\left(\mathrm{ndx}\right)$$
7	6	opeq1i	$$⊢⟨N,\underset{\dot{}}{+}⟩=⟨\mathrm{Slot}N\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩$$
8	7	preq2i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Slot}N\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}$$
9	1 8	eqtri	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Slot}N\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}$$
10		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
11	10 2	eqbrtrri	$$⊢1<N$$
12	9 4 11 3	2strstr	$$⊢G\mathrm{Struct}⟨1,N⟩$$
13	10	opeq1i	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},N⟩=⟨1,N⟩$$
14	12 13	breqtrri	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},N⟩$$