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	$$⊢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		basendxnn	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathbb{N}$$
5		eqid	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}={\mathrm{Base}}_{\mathrm{ndx}}$$
6		eqid	$$⊢N=N$$
7	4 5 2 3 6	strle2	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},N⟩$$
8	1 7	eqbrtri	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},N⟩$$