Theorem opelstrbas

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

	Ref	Expression
Hypotheses	opelstrbas.s	$$⊢\phi \to S\mathrm{Struct}X$$
	opelstrbas.v	$$⊢\phi \to V\in Y$$
	opelstrbas.b	$$⊢\phi \to ⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in S$$
Assertion	opelstrbas	$$⊢\phi \to V={\mathrm{Base}}_S$$

Proof

Step	Hyp	Ref	Expression
1		opelstrbas.s	$$⊢\phi \to S\mathrm{Struct}X$$
2		opelstrbas.v	$$⊢\phi \to V\in Y$$
3		opelstrbas.b	$$⊢\phi \to ⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in S$$
4		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
5		structex	$$⊢S\mathrm{Struct}X\to S\in \mathrm{V}$$
6	1 5	syl	$$⊢\phi \to S\in \mathrm{V}$$
7		structfung	$$⊢S\mathrm{Struct}X\to \mathrm{Fun}{S^{-1}}^{-1}$$
8	1 7	syl	$$⊢\phi \to \mathrm{Fun}{S^{-1}}^{-1}$$
9	4 6 8 3 2	strfv2d	$$⊢\phi \to V={\mathrm{Base}}_S$$