Metamath Proof Explorer


Theorem 2strop

Description: The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015) Use the index-independent version 2strop1 instead. (New usage is discouraged.)

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 ) )