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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}$$
Assertion	1strstr	$$⊢G\mathrm{Struct}⟨1,1⟩$$

Proof

Step	Hyp	Ref	Expression
1		1str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}$$
2		1nn	$$⊢1\in \mathbb{N}$$
3		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
4	2 3	strle1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}\mathrm{Struct}⟨1,1⟩$$
5	1 4	eqbrtri	$$⊢G\mathrm{Struct}⟨1,1⟩$$