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	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
	basvtxval.d	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
	basvtxval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑌 )
	basvtxval.b	⊢ ( 𝜑 → ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 )
Assertion	basvtxval	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		basvtxval.s	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
2		basvtxval.d	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
3		basvtxval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑌 )
4		basvtxval.b	⊢ ( 𝜑 → ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 )
5		structn0fun	⊢ ( 𝐺 Struct 𝑋 → Fun ( 𝐺 ∖ { ∅ } ) )
6	1 5	syl	⊢ ( 𝜑 → Fun ( 𝐺 ∖ { ∅ } ) )
7		funvtxdmge2val	⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
8	6 2 7	syl2anc	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
9	1 3 4	opelstrbas	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝐺 ) )
10	8 9	eqtr4d	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )