This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		basvtxval.s	$⊢ φ \to G Struct X$
2		basvtxval.d	$⊢ φ \to 2 \leq \|dom G\|$
3		basvtxval.v	$⊢ φ \to V \in Y$
4		basvtxval.b	$⊢ φ \to ⟨{Base}_{ndx}, V⟩ \in G$
5		structn0fun	$⊢ G Struct X \to Fun (G ∖ \{\emptyset\})$
6	1 5	syl	$⊢ φ \to Fun (G ∖ \{\emptyset\})$
7		funvtxdmge2val	$⊢ (Fun (G ∖ \{\emptyset\}) \land 2 \leq \|dom G\|) \to Vtx (G) = {Base}_{G}$
8	6 2 7	syl2anc	$⊢ φ \to Vtx (G) = {Base}_{G}$
9	1 3 4	opelstrbas	$⊢ φ \to V = {Base}_{G}$
10	8 9	eqtr4d	$⊢ φ \to Vtx (G) = V$