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 )