Theorem 2strop1

Description: The other slot of a constructed two-slot structure. Version of 2strop 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
	2str1.e	|- E = Slot N
Assertion	2strop1	|- ( .+ e. V -> .+ = ( E ` 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		2str1.e	|- E = Slot N
5	1 2 3	2strstr1	|- G Struct <. ( Base ` ndx ) , N >.
6	4 3	ndxid	|- E = Slot ( E ` ndx )
7		snsspr2	|- { <. N , .+ >. } C_ { <. ( Base ` ndx ) , B >. , <. N , .+ >. }
8	4 3	ndxarg	|- ( E ` ndx ) = N
9	8	opeq1i	|- <. ( E ` ndx ) , .+ >. = <. N , .+ >.
10	9	sneqi	|- { <. ( E ` ndx ) , .+ >. } = { <. N , .+ >. }
11	7 10 1	3sstr4i	|- { <. ( E ` ndx ) , .+ >. } C_ G
12	5 6 11	strfv	|- ( .+ e. V -> .+ = ( E ` G ) )