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

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 
|- ( ph -> G Struct X )
structgrssvtx.v 
|- ( ph -> V e. Y )
structgrssvtx.e 
|- ( ph -> E e. Z )
structgrssvtx.s 
|- ( ph -> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
Assertion structgrssvtx 
|- ( ph -> ( Vtx ` G ) = V )

Proof

Step Hyp Ref Expression
1 structgrssvtx.g 
 |-  ( ph -> G Struct X )
2 structgrssvtx.v 
 |-  ( ph -> V e. Y )
3 structgrssvtx.e 
 |-  ( ph -> E e. Z )
4 structgrssvtx.s 
 |-  ( ph -> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
5 1 2 3 4 structgrssvtxlem 
 |-  ( ph -> 2 <_ ( # ` dom G ) )
6 opex 
 |-  <. ( Base ` ndx ) , V >. e. _V
7 opex 
 |-  <. ( .ef ` ndx ) , E >. e. _V
8 6 7 prss 
 |-  ( ( <. ( Base ` ndx ) , V >. e. G /\ <. ( .ef ` ndx ) , E >. e. G ) <-> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
9 simpl 
 |-  ( ( <. ( Base ` ndx ) , V >. e. G /\ <. ( .ef ` ndx ) , E >. e. G ) -> <. ( Base ` ndx ) , V >. e. G )
10 8 9 sylbir 
 |-  ( { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G -> <. ( Base ` ndx ) , V >. e. G )
11 4 10 syl 
 |-  ( ph -> <. ( Base ` ndx ) , V >. e. G )
12 1 5 2 11 basvtxval 
 |-  ( ph -> ( Vtx ` G ) = V )