This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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