Theorem 1strstr1

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

	Ref	Expression
Hypothesis	1str.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
Assertion	1strstr1	⊢ 𝐺 Struct ⟨ ( Base ‘ ndx ) , ( Base ‘ ndx ) ⟩

Proof

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