Theorem 2strbas1

Description: The base set of a constructed two-slot structure. Version of 2strbas 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	2strbas1	|- ( B e. V -> B = ( Base ` G ) )

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	1 2 3	2strstr1	|- G Struct <. ( Base ` ndx ) , N >.
5		baseid	|- Base = Slot ( Base ` ndx )
6		snsspr1	|- { <. ( Base ` ndx ) , B >. } C_ { <. ( Base ` ndx ) , B >. , <. N , .+ >. }
7	6 1	sseqtrri	|- { <. ( Base ` ndx ) , B >. } C_ G
8	4 5 7	strfv	|- ( B e. V -> B = ( Base ` G ) )