This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2strop

Description: The other slot 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
2str.e 
|- E = Slot N
Assertion 2strop 
|- ( .+ e. V -> .+ = ( E ` 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 2str.e 
 |-  E = Slot N
5 1 2 3 2strstr 
 |-  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 ) )