Metamath Proof Explorer


Theorem 2strbas1

Description: The base set of a constructed two-slot structure. Version of 2strbas 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
Assertion 2strbas1
|- ( B e. V -> B = ( Base ` 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 1 2 3 2strstr1
 |-  G Struct <. ( Base ` ndx ) , N >.
5 baseid
 |-  Base = Slot ( Base ` ndx )
6 snsspr1
 |-  { <. ( Base ` ndx ) , B >. } C_ { <. ( Base ` ndx ) , B >. , <. N , .+ >. }
7 6 1 sseqtrri
 |-  { <. ( Base ` ndx ) , B >. } C_ G
8 4 5 7 strfv
 |-  ( B e. V -> B = ( Base ` G ) )