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	$$⊢\phi \to G\mathrm{Struct}X$$
	basvtxval.d	$$⊢\phi \to 2\le \left|\mathrm{dom}G\right|$$
	basvtxval.v	$$⊢\phi \to V\in Y$$
	basvtxval.b	$$⊢\phi \to ⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in G$$
Assertion	basvtxval	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		basvtxval.s	$$⊢\phi \to G\mathrm{Struct}X$$
2		basvtxval.d	$$⊢\phi \to 2\le \left|\mathrm{dom}G\right|$$
3		basvtxval.v	$$⊢\phi \to V\in Y$$
4		basvtxval.b	$$⊢\phi \to ⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in G$$
5		structn0fun	$$⊢G\mathrm{Struct}X\to \mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)$$
6	1 5	syl	$$⊢\phi \to \mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)$$
7		funvtxdmge2val	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge 2\le \left|\mathrm{dom}G\right|\right)\to \mathrm{Vtx}\left(G\right)={\mathrm{Base}}_G$$
8	6 2 7	syl2anc	$$⊢\phi \to \mathrm{Vtx}\left(G\right)={\mathrm{Base}}_G$$
9	1 3 4	opelstrbas	$$⊢\phi \to V={\mathrm{Base}}_G$$
10	8 9	eqtr4d	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$