Metamath Proof Explorer


Theorem structgrssvtx

Description: The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020) (Proof shortened by AV, 12-Nov-2021)

Ref Expression
Hypotheses structgrssvtx.g ( 𝜑𝐺 Struct 𝑋 )
structgrssvtx.v ( 𝜑𝑉𝑌 )
structgrssvtx.e ( 𝜑𝐸𝑍 )
structgrssvtx.s ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 )
Assertion structgrssvtx ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )

Proof

Step Hyp Ref Expression
1 structgrssvtx.g ( 𝜑𝐺 Struct 𝑋 )
2 structgrssvtx.v ( 𝜑𝑉𝑌 )
3 structgrssvtx.e ( 𝜑𝐸𝑍 )
4 structgrssvtx.s ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 )
5 1 2 3 4 structgrssvtxlem ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
6 opex ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ V
7 opex ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ V
8 6 7 prss ( ( ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 ∧ ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ 𝐺 ) ↔ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 )
9 simpl ( ( ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 ∧ ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ 𝐺 ) → ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 )
10 8 9 sylbir ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 → ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 )
11 4 10 syl ( 𝜑 → ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 )
12 1 5 2 11 basvtxval ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )