This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem umgredg2

Description: An edge of a multigraph has exactly two ends. (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v 
|- V = ( Vtx ` G )
isumgr.e 
|- E = ( iEdg ` G )
Assertion umgredg2 
|- ( ( G e. UMGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )

Proof

Step Hyp Ref Expression
1 isumgr.v 
 |-  V = ( Vtx ` G )
2 isumgr.e 
 |-  E = ( iEdg ` G )
3 1 2 umgrf 
 |-  ( G e. UMGraph -> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } )
4 3 ffvelcdmda 
 |-  ( ( G e. UMGraph /\ X e. dom E ) -> ( E ` X ) e. { x e. ~P V | ( # ` x ) = 2 } )
5 fveqeq2 
 |-  ( x = ( E ` X ) -> ( ( # ` x ) = 2 <-> ( # ` ( E ` X ) ) = 2 ) )
6 5 elrab 
 |-  ( ( E ` X ) e. { x e. ~P V | ( # ` x ) = 2 } <-> ( ( E ` X ) e. ~P V /\ ( # ` ( E ` X ) ) = 2 ) )
7 6 simprbi 
 |-  ( ( E ` X ) e. { x e. ~P V | ( # ` x ) = 2 } -> ( # ` ( E ` X ) ) = 2 )
8 4 7 syl 
 |-  ( ( G e. UMGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )