Theorem 2strbas

Description: The base set of a constructed two-slot structure not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020)

	Ref	Expression
Hypotheses	2str.g	|- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. }
	2str.b	|- ( Base ` ndx ) < N
	2str.n	|- N e. NN
Assertion	2strbas	|- ( B e. V -> B = ( Base ` G ) )

Proof

Step	Hyp	Ref	Expression
1		2str.g	|- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. }
2		2str.b	|- ( Base ` ndx ) < N
3		2str.n	|- N e. NN
4	1 2 3	2strstr	|- 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 ) )