Theorem opelstrbas

Description: The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021)

	Ref	Expression
Hypotheses	opelstrbas.s	⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
	opelstrbas.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑌 )
	opelstrbas.b	⊢ ( 𝜑 → ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝑆 )
Assertion	opelstrbas	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		opelstrbas.s	⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
2		opelstrbas.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑌 )
3		opelstrbas.b	⊢ ( 𝜑 → ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝑆 )
4		baseid	⊢ Base = Slot ( Base ‘ ndx )
5		structex	⊢ ( 𝑆 Struct 𝑋 → 𝑆 ∈ V )
6	1 5	syl	⊢ ( 𝜑 → 𝑆 ∈ V )
7		structfung	⊢ ( 𝑆 Struct 𝑋 → Fun ◡ ◡ 𝑆 )
8	1 7	syl	⊢ ( 𝜑 → Fun ◡ ◡ 𝑆 )
9	4 6 8 3 2	strfv2d	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑆 ) )