Theorem 2strbas

Description: The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015)

	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	2strbas	|- ( B e. V -> B = ( Base ` G ) )

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