Theorem 1strstr1

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

	Ref	Expression
Hypothesis	1str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}$$
Assertion	1strstr1	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\mathrm{ndx}}⟩$$

Proof

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