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

Metamath Proof Explorer

Theorem usgrexmplvtx

Description: The vertices 0 , 1 , 2 , 3 , 4 of the graph G = <. V , E >. . (Contributed by AV, 12-Jan-2020) (Revised by AV, 21-Oct-2020)

Ref Expression
Hypotheses usgrexmpl.v 
|- V = ( 0 ... 4 )
usgrexmpl.e 
|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">
usgrexmpl.g 
|- G = <. V , E >.
Assertion usgrexmplvtx 
|- ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )

Proof

Step Hyp Ref Expression
1 usgrexmpl.v 
 |-  V = ( 0 ... 4 )
2 usgrexmpl.e 
 |-  E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">
3 usgrexmpl.g 
 |-  G = <. V , E >.
4 1 2 3 usgrexmpllem 
 |-  ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E )
5 id 
 |-  ( ( Vtx ` G ) = V -> ( Vtx ` G ) = V )
6 fz0to4untppr 
 |-  ( 0 ... 4 ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )
7 1 6 eqtri 
 |-  V = ( { 0 , 1 , 2 } u. { 3 , 4 } )
8 5 7 eqtrdi 
 |-  ( ( Vtx ` G ) = V -> ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } ) )
9 8 adantr 
 |-  ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } ) )
10 4 9 ax-mp 
 |-  ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )