Theorem funvtxval

Description: The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 22-Sep-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

	Ref	Expression
Assertion	funvtxval	⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom 𝐺 ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		basendxnedgfndx	⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx )
2		fvex	⊢ ( Base ‘ ndx ) ∈ V
3		fvex	⊢ ( .ef ‘ ndx ) ∈ V
4	2 3	funvtxdm2val	⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx ) ∧ { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom 𝐺 ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
5	1 4	mp3an2	⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom 𝐺 ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )