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 = { <. ( 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		basendxnn	|- ( Base ` ndx ) e. NN
5		eqid	|- ( Base ` ndx ) = ( Base ` ndx )
6		eqid	|- N = N
7	4 5 2 3 6	strle2	|- { <. ( Base ` ndx ) , B >. , <. N , .+ >. } Struct <. ( Base ` ndx ) , N >.
8	1 7	eqbrtri	|- G Struct <. ( Base ` ndx ) , N >.