Theorem 2strop

Description: The other slot 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	2strop	|- ( .+ e. V -> .+ = ( E ` 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	2 4	ndxid	|- E = Slot ( E ` ndx )
7		snsspr2	|- { <. ( E ` ndx ) , .+ >. } C_ { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }
8	7 1	sseqtrri	|- { <. ( E ` ndx ) , .+ >. } C_ G
9	5 6 8	strfv	|- ( .+ e. V -> .+ = ( E ` G ) )