Metamath Proof Explorer


Theorem 2strbas

Description: The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015) Use the index-independent version 2strbas1 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 2strbas
|- ( B e. V -> B = ( Base ` 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 baseid
 |-  Base = Slot ( Base ` ndx )
7 snsspr1
 |-  { <. ( Base ` ndx ) , B >. } C_ { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }
8 7 1 sseqtrri
 |-  { <. ( Base ` ndx ) , B >. } C_ G
9 5 6 8 strfv
 |-  ( B e. V -> B = ( Base ` G ) )