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 ordered pair opvtxfvi
Description: The set of vertices of a graph represented as an ordered pair of
vertices and indexed edges as function value. (Contributed by AV , 4-Mar-2021)
Ref
Expression
Hypotheses
opvtxfvi.v ⊢ 𝑉 ∈ V
opvtxfvi.e ⊢ 𝐸 ∈ V
Assertion
opvtxfvi ⊢ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉
Proof
Step
Hyp
Ref
Expression
1
opvtxfvi.v ⊢ 𝑉 ∈ V
2
opvtxfvi.e ⊢ 𝐸 ∈ V
3
opvtxfv ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
4
1 2 3
mp2an ⊢ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉