Metamath Proof Explorer


Theorem 2strstr1

Description: A constructed two-slot structure. Version of 2strstr 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 2strstr1
|- G Struct <. ( Base ` ndx ) , N >.

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 eqid
 |-  Slot N = Slot N
5 4 3 ndxarg
 |-  ( Slot N ` ndx ) = N
6 5 eqcomi
 |-  N = ( Slot N ` ndx )
7 6 opeq1i
 |-  <. N , .+ >. = <. ( Slot N ` ndx ) , .+ >.
8 7 preq2i
 |-  { <. ( Base ` ndx ) , B >. , <. N , .+ >. } = { <. ( Base ` ndx ) , B >. , <. ( Slot N ` ndx ) , .+ >. }
9 1 8 eqtri
 |-  G = { <. ( Base ` ndx ) , B >. , <. ( Slot N ` ndx ) , .+ >. }
10 basendx
 |-  ( Base ` ndx ) = 1
11 10 2 eqbrtrri
 |-  1 < N
12 9 4 11 3 2strstr
 |-  G Struct <. 1 , N >.
13 10 opeq1i
 |-  <. ( Base ` ndx ) , N >. = <. 1 , N >.
14 12 13 breqtrri
 |-  G Struct <. ( Base ` ndx ) , N >.