Metamath Proof Explorer

Theorem wrdumgr

Description: The property of being an undirected multigraph, expressing the edges as "words". (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v 
|- V = ( Vtx ` G )
isumgr.e 
|- E = ( iEdg ` G )
Assertion wrdumgr 
|- ( ( G e. U /\ E e. Word X ) -> ( G e. UMGraph <-> E e. Word { x e. ~P V | ( # ` x ) = 2 } ) )

Proof

Step Hyp Ref Expression
1 isumgr.v 
 |-  V = ( Vtx ` G )
2 isumgr.e 
 |-  E = ( iEdg ` G )
3 1 2 isumgrs 
 |-  ( G e. U -> ( G e. UMGraph <-> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } ) )
4 3 adantr 
 |-  ( ( G e. U /\ E e. Word X ) -> ( G e. UMGraph <-> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } ) )
5 wrdf 
 |-  ( E e. Word X -> E : ( 0 ..^ ( # ` E ) ) --> X )
6 5 adantl 
 |-  ( ( G e. U /\ E e. Word X ) -> E : ( 0 ..^ ( # ` E ) ) --> X )
7 6 fdmd 
 |-  ( ( G e. U /\ E e. Word X ) -> dom E = ( 0 ..^ ( # ` E ) ) )
8 7 feq2d 
 |-  ( ( G e. U /\ E e. Word X ) -> ( E : dom E --> { x e. ~P V | ( # ` x ) = 2 } <-> E : ( 0 ..^ ( # ` E ) ) --> { x e. ~P V | ( # ` x ) = 2 } ) )
9 iswrdi 
 |-  ( E : ( 0 ..^ ( # ` E ) ) --> { x e. ~P V | ( # ` x ) = 2 } -> E e. Word { x e. ~P V | ( # ` x ) = 2 } )
10 wrdf 
 |-  ( E e. Word { x e. ~P V | ( # ` x ) = 2 } -> E : ( 0 ..^ ( # ` E ) ) --> { x e. ~P V | ( # ` x ) = 2 } )
11 9 10 impbii 
 |-  ( E : ( 0 ..^ ( # ` E ) ) --> { x e. ~P V | ( # ` x ) = 2 } <-> E e. Word { x e. ~P V | ( # ` x ) = 2 } )
12 8 11 bitrdi 
 |-  ( ( G e. U /\ E e. Word X ) -> ( E : dom E --> { x e. ~P V | ( # ` x ) = 2 } <-> E e. Word { x e. ~P V | ( # ` x ) = 2 } ) )
13 4 12 bitrd 
 |-  ( ( G e. U /\ E e. Word X ) -> ( G e. UMGraph <-> E e. Word { x e. ~P V | ( # ` x ) = 2 } ) )