Metamath Proof Explorer

Theorem 1strstr

Description: A constructed one-slot structure. (Contributed by AV, 27-Mar-2020)

Ref Expression
Hypothesis 1str.g 
|- G = { <. ( Base ` ndx ) , B >. }
Assertion 1strstr 
|- G Struct <. 1 , 1 >.

Proof

Step Hyp Ref Expression
1 1str.g 
 |-  G = { <. ( Base ` ndx ) , B >. }
2 1nn 
 |-  1 e. NN
3 basendx 
 |-  ( Base ` ndx ) = 1
4 2 3 strle1 
 |-  { <. ( Base ` ndx ) , B >. } Struct <. 1 , 1 >.
5 1 4 eqbrtri 
 |-  G Struct <. 1 , 1 >.