Theorem 1strstr

Description: A constructed one-slot structure. Depending on hard-coded index. Use 1strstr1 instead. (Contributed by AV, 27-Mar-2020) (New usage is discouraged.)

	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 >.