Theorem 1strstr1

Description: A constructed one-slot structure. (Contributed by AV, 15-Nov-2024)

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

Proof

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