Metamath Proof Explorer

Theorem konigsbergumgr

Description: The Königsberg graph G is a multigraph. (Contributed by AV, 28-Feb-2021) (Revised by AV, 9-Mar-2021)

Ref Expression
Hypotheses konigsberg.v 
|- V = ( 0 ... 3 )
konigsberg.e 
|- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">
konigsberg.g 
|- G = <. V , E >.
Assertion konigsbergumgr 
|- G e. UMGraph

Proof

Step Hyp Ref Expression
1 konigsberg.v 
 |-  V = ( 0 ... 3 )
2 konigsberg.e 
 |-  E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">
3 konigsberg.g 
 |-  G = <. V , E >.
4 1 2 3 konigsbergiedgw 
 |-  E e. Word { x e. ~P V | ( # ` x ) = 2 }
5 opex 
 |-  <. V , E >. e. _V
6 3 5 eqeltri 
 |-  G e. _V
7 s7cli 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. Word _V
8 2 7 eqeltri 
 |-  E e. Word _V
9 1 2 3 konigsbergvtx 
 |-  ( Vtx ` G ) = ( 0 ... 3 )
10 1 9 eqtr4i 
 |-  V = ( Vtx ` G )
11 1 2 3 konigsbergiedg 
 |-  ( iEdg ` G ) = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">
12 2 11 eqtr4i 
 |-  E = ( iEdg ` G )
13 10 12 wrdumgr 
 |-  ( ( G e. _V /\ E e. Word _V ) -> ( G e. UMGraph <-> E e. Word { x e. ~P V | ( # ` x ) = 2 } ) )
14 6 8 13 mp2an 
 |-  ( G e. UMGraph <-> E e. Word { x e. ~P V | ( # ` x ) = 2 } )
15 4 14 mpbir 
 |-  G e. UMGraph