Metamath Proof Explorer

Theorem usgrexmpl1vtx

Description: The vertices 0 , 1 , 2 , 3 , 4 , 5 of the graph G = <. V , E >. . (Contributed by AV, 3-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 usgrexmpl1.v 
 |-  V = ( 0 ... 5 )
2 usgrexmpl1.e 
 |-  E = <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ">
3 usgrexmpl1.g 
 |-  G = <. V , E >.
4 3 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` <. V , E >. )
5 1 ovexi 
 |-  V e. _V
6 s7cli 
 |-  <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } "> e. Word _V
7 2 6 eqeltri 
 |-  E e. Word _V
8 opvtxfv 
 |-  ( ( V e. _V /\ E e. Word _V ) -> ( Vtx ` <. V , E >. ) = V )
9 5 7 8 mp2an 
 |-  ( Vtx ` <. V , E >. ) = V
10 4 9 eqtri 
 |-  ( Vtx ` G ) = V
11 fz0to5un2tp 
 |-  ( 0 ... 5 ) = ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
12 10 1 11 3eqtri 
 |-  ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )