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 )