Theorem umgredgnlp

Description: An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020) (Revised by AV, 8-Jun-2021)

	Ref	Expression
Hypothesis	umgredgnlp.e	|- E = ( Edg ` G )
Assertion	umgredgnlp	|- ( ( G e. UMGraph /\ C e. E ) -> -. E. v C = { v } )

Proof

Step	Hyp	Ref	Expression
1		umgredgnlp.e	|- E = ( Edg ` G )
2		vex	|- v e. _V
3		hashsng	|- ( v e. _V -> ( # ` { v } ) = 1 )
4		1ne2	|- 1 =/= 2
5	4	neii	|- -. 1 = 2
6		eqeq1	|- ( ( # ` { v } ) = 1 -> ( ( # ` { v } ) = 2 <-> 1 = 2 ) )
7	5 6	mtbiri	|- ( ( # ` { v } ) = 1 -> -. ( # ` { v } ) = 2 )
8	2 3 7	mp2b	|- -. ( # ` { v } ) = 2
9		fveqeq2	|- ( C = { v } -> ( ( # ` C ) = 2 <-> ( # ` { v } ) = 2 ) )
10	8 9	mtbiri	|- ( C = { v } -> -. ( # ` C ) = 2 )
11	10	intnand	|- ( C = { v } -> -. ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
12	1	eleq2i	|- ( C e. E <-> C e. ( Edg ` G ) )
13		edgumgr	|- ( ( G e. UMGraph /\ C e. ( Edg ` G ) ) -> ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
14	12 13	sylan2b	|- ( ( G e. UMGraph /\ C e. E ) -> ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
15	11 14	nsyl3	|- ( ( G e. UMGraph /\ C e. E ) -> -. C = { v } )
16	15	nexdv	|- ( ( G e. UMGraph /\ C e. E ) -> -. E. v C = { v } )