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 = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }
	2str.e	|- E = Slot N
	2str.l	|- 1 < N
	2str.n	|- N e. NN
Assertion	2strstr	|- G Struct <. 1 , N >.

Proof

Step	Hyp	Ref	Expression
1		2str.g	|- G = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }
2		2str.e	|- E = Slot N
3		2str.l	|- 1 < N
4		2str.n	|- N e. NN
5		1nn	|- 1 e. NN
6		basendx	|- ( Base ` ndx ) = 1
7	2 4	ndxarg	|- ( E ` ndx ) = N
8	5 6 3 4 7	strle2	|- { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. } Struct <. 1 , N >.
9	1 8	eqbrtri	|- G Struct <. 1 , N >.