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 = { <. ( Base ` ndx ) , B >. , <. N , .+ >. }
	2str1.b	|- ( Base ` ndx ) < N
	2str1.n	|- N e. NN
Assertion	2strstr1	|- G Struct <. ( Base ` ndx ) , N >.

Proof

Step	Hyp	Ref	Expression
1		2str1.g	|- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. }
2		2str1.b	|- ( Base ` ndx ) < N
3		2str1.n	|- N e. NN
4		eqid	|- Slot N = Slot N
5	4 3	ndxarg	|- ( Slot N ` ndx ) = N
6	5	eqcomi	|- N = ( Slot N ` ndx )
7	6	opeq1i	|- <. N , .+ >. = <. ( Slot N ` ndx ) , .+ >.
8	7	preq2i	|- { <. ( Base ` ndx ) , B >. , <. N , .+ >. } = { <. ( Base ` ndx ) , B >. , <. ( Slot N ` ndx ) , .+ >. }
9	1 8	eqtri	|- G = { <. ( Base ` ndx ) , B >. , <. ( Slot N ` ndx ) , .+ >. }
10		basendx	|- ( Base ` ndx ) = 1
11	10 2	eqbrtrri	|- 1 < N
12	9 4 11 3	2strstr	|- G Struct <. 1 , N >.
13	10	opeq1i	|- <. ( Base ` ndx ) , N >. = <. 1 , N >.
14	12 13	breqtrri	|- G Struct <. ( Base ` ndx ) , N >.