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	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
Assertion	1strstr	⊢ 𝐺 Struct ⟨ 1 , 1 ⟩

Proof

Step	Hyp	Ref	Expression
1		1str.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
2		1nn	⊢ 1 ∈ ℕ
3		basendx	⊢ ( Base ‘ ndx ) = 1
4	2 3	strle1	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } Struct ⟨ 1 , 1 ⟩
5	1 4	eqbrtri	⊢ 𝐺 Struct ⟨ 1 , 1 ⟩