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) (Proof shortened by AV, 17-Oct-2024)

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 basendxnn
 |-  ( Base ` ndx ) e. NN
5 eqid
 |-  ( Base ` ndx ) = ( Base ` ndx )
6 eqid
 |-  N = N
7 4 5 2 3 6 strle2
 |-  { <. ( Base ` ndx ) , B >. , <. N , .+ >. } Struct <. ( Base ` ndx ) , N >.
8 1 7 eqbrtri
 |-  G Struct <. ( Base ` ndx ) , N >.