Theorem 1strbas

Description: The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020) (Proof shortened by AV, 15-Nov-2024)

	Ref	Expression
Hypothesis	1str.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
Assertion	1strbas	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		1str.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
2	1	1strstr	⊢ 𝐺 Struct ⟨ ( Base ‘ ndx ) , ( Base ‘ ndx ) ⟩
3		baseid	⊢ Base = Slot ( Base ‘ ndx )
4	1	eqimss2i	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ 𝐺
5	2 3 4	strfv	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐺 ) )