Metamath Proof Explorer

Theorem usgrexmpllem

Description: Lemma for usgrexmpl . (Contributed 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 usgrexmpllem 
|- ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E )

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 ovexi 
 |-  V e. _V
5 s4cli 
 |-  <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> e. Word _V
6 5 elexi 
 |-  <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> e. _V
7 2 6 eqeltri 
 |-  E e. _V
8 opvtxfv 
 |-  ( ( V e. _V /\ E e. _V ) -> ( Vtx ` <. V , E >. ) = V )
9 opiedgfv 
 |-  ( ( V e. _V /\ E e. _V ) -> ( iEdg ` <. V , E >. ) = E )
10 8 9 jca 
 |-  ( ( V e. _V /\ E e. _V ) -> ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) )
11 4 7 10 mp2an 
 |-  ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E )
12 3 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` <. V , E >. )
13 12 eqeq1i 
 |-  ( ( Vtx ` G ) = V <-> ( Vtx ` <. V , E >. ) = V )
14 3 fveq2i 
 |-  ( iEdg ` G ) = ( iEdg ` <. V , E >. )
15 14 eqeq1i 
 |-  ( ( iEdg ` G ) = E <-> ( iEdg ` <. V , E >. ) = E )
16 13 15 anbi12i 
 |-  ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) <-> ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) )
17 11 16 mpbir 
 |-  ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E )