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 ( 𝜑𝐺 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 ‘ 𝐺 ) = 𝑉 )