Theorem opelstrbas

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

	Ref	Expression
Hypotheses	opelstrbas.s	|- ( ph -> S Struct X )
	opelstrbas.v	|- ( ph -> V e. Y )
	opelstrbas.b	|- ( ph -> <. ( Base ` ndx ) , V >. e. S )
Assertion	opelstrbas	|- ( ph -> V = ( Base ` S ) )

Proof

Step	Hyp	Ref	Expression
1		opelstrbas.s	|- ( ph -> S Struct X )
2		opelstrbas.v	|- ( ph -> V e. Y )
3		opelstrbas.b	|- ( ph -> <. ( Base ` ndx ) , V >. e. S )
4		baseid	|- Base = Slot ( Base ` ndx )
5		structex	|- ( S Struct X -> S e. _V )
6	1 5	syl	|- ( ph -> S e. _V )
7		structfung	|- ( S Struct X -> Fun `' `' S )
8	1 7	syl	|- ( ph -> Fun `' `' S )
9	4 6 8 3 2	strfv2d	|- ( ph -> V = ( Base ` S ) )