Metamath Proof Explorer


Theorem usgrexmpl

Description: G is a simple graph of five vertices 0 , 1 , 2 , 3 , 4 , with edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } . (Contributed by Alexander van der Vekens, 15-Aug-2017) (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 usgrexmpl
|- G e. USGraph

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 usgrexmplef
 |-  E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 }
5 opex
 |-  <. V , E >. e. _V
6 3 5 eqeltri
 |-  G e. _V
7 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 eqid
 |-  ( iEdg ` G ) = ( iEdg ` G )
9 7 8 isusgrs
 |-  ( G e. _V -> ( G e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } ) )
10 1 2 3 usgrexmpllem
 |-  ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E )
11 simpr
 |-  ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ( iEdg ` G ) = E )
12 11 dmeqd
 |-  ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> dom ( iEdg ` G ) = dom E )
13 pweq
 |-  ( ( Vtx ` G ) = V -> ~P ( Vtx ` G ) = ~P V )
14 13 adantr
 |-  ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ~P ( Vtx ` G ) = ~P V )
15 14 rabeqdv
 |-  ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } = { e e. ~P V | ( # ` e ) = 2 } )
16 11 12 15 f1eq123d
 |-  ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } ) )
17 10 16 ax-mp
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
18 9 17 bitrdi
 |-  ( G e. _V -> ( G e. USGraph <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } ) )
19 6 18 ax-mp
 |-  ( G e. USGraph <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
20 4 19 mpbir
 |-  G e. USGraph