This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Vertices and edges Vertices and indexed edges The vertices and edges of a graph represented as extensible structure funvtxval0
Description: The set of vertices of an extensible structure with a base set and (at
least) another slot. (Contributed by AV , 22-Sep-2020) (Revised by AV , 7-Jun-2021) (Revised by AV , 12-Nov-2021)
Ref
Expression
Hypothesis
funvtxval0.s ⊢ 𝑆 ∈ V
Assertion
funvtxval0 ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝑆 ≠ ( Base ‘ ndx ) ∧ { ( Base ‘ ndx ) , 𝑆 } ⊆ dom 𝐺 ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
Proof
Step
Hyp
Ref
Expression
1
funvtxval0.s ⊢ 𝑆 ∈ V
2
necom ⊢ ( 𝑆 ≠ ( Base ‘ ndx ) ↔ ( Base ‘ ndx ) ≠ 𝑆 )
3
fvex ⊢ ( Base ‘ ndx ) ∈ V
4
3 1
funvtxdm2val ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ ( Base ‘ ndx ) ≠ 𝑆 ∧ { ( Base ‘ ndx ) , 𝑆 } ⊆ dom 𝐺 ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
5
2 4
syl3an2b ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝑆 ≠ ( Base ‘ ndx ) ∧ { ( Base ‘ ndx ) , 𝑆 } ⊆ dom 𝐺 ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )