Theorem basvtxval

Description: The set of vertices of a graph represented as an extensible structure with the set of vertices as base set. (Contributed by AV, 14-Oct-2020) (Revised by AV, 12-Nov-2021)

	Ref	Expression
Hypotheses	basvtxval.s	|- ( ph -> G Struct X )
	basvtxval.d	|- ( ph -> 2 <_ ( # ` dom G ) )
	basvtxval.v	|- ( ph -> V e. Y )
	basvtxval.b	|- ( ph -> <. ( Base ` ndx ) , V >. e. G )
Assertion	basvtxval	|- ( ph -> ( Vtx ` G ) = V )

Proof

Step	Hyp	Ref	Expression
1		basvtxval.s	|- ( ph -> G Struct X )
2		basvtxval.d	|- ( ph -> 2 <_ ( # ` dom G ) )
3		basvtxval.v	|- ( ph -> V e. Y )
4		basvtxval.b	|- ( ph -> <. ( Base ` ndx ) , V >. e. G )
5		structn0fun	|- ( G Struct X -> Fun ( G \ { (/) } ) )
6	1 5	syl	|- ( ph -> Fun ( G \ { (/) } ) )
7		funvtxdmge2val	|- ( ( Fun ( G \ { (/) } ) /\ 2 <_ ( # ` dom G ) ) -> ( Vtx ` G ) = ( Base ` G ) )
8	6 2 7	syl2anc	|- ( ph -> ( Vtx ` G ) = ( Base ` G ) )
9	1 3 4	opelstrbas	|- ( ph -> V = ( Base ` G ) )
10	8 9	eqtr4d	|- ( ph -> ( Vtx ` G ) = V )