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	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}$$
	2str.e	$$⊢E=\mathrm{Slot}N$$
	2str.l	$$⊢1<N$$
	2str.n	$$⊢N\in \mathbb{N}$$
Assertion	2strstr	$$⊢G\mathrm{Struct}⟨1,N⟩$$

Proof

Step	Hyp	Ref	Expression
1		2str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}$$
2		2str.e	$$⊢E=\mathrm{Slot}N$$
3		2str.l	$$⊢1<N$$
4		2str.n	$$⊢N\in \mathbb{N}$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
7	2 4	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$
8	5 6 3 4 7	strle2	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}\mathrm{Struct}⟨1,N⟩$$
9	1 8	eqbrtri	$$⊢G\mathrm{Struct}⟨1,N⟩$$