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	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	umgredgnlp	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸 ) → ¬ ∃ 𝑣 𝐶 = { 𝑣 } )

Proof

Step	Hyp	Ref	Expression
1		umgredgnlp.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2		vex	⊢ 𝑣 ∈ V
3		hashsng	⊢ ( 𝑣 ∈ V → ( ♯ ‘ { 𝑣 } ) = 1 )
4		1ne2	⊢ 1 ≠ 2
5	4	neii	⊢ ¬ 1 = 2
6		eqeq1	⊢ ( ( ♯ ‘ { 𝑣 } ) = 1 → ( ( ♯ ‘ { 𝑣 } ) = 2 ↔ 1 = 2 ) )
7	5 6	mtbiri	⊢ ( ( ♯ ‘ { 𝑣 } ) = 1 → ¬ ( ♯ ‘ { 𝑣 } ) = 2 )
8	2 3 7	mp2b	⊢ ¬ ( ♯ ‘ { 𝑣 } ) = 2
9		fveqeq2	⊢ ( 𝐶 = { 𝑣 } → ( ( ♯ ‘ 𝐶 ) = 2 ↔ ( ♯ ‘ { 𝑣 } ) = 2 ) )
10	8 9	mtbiri	⊢ ( 𝐶 = { 𝑣 } → ¬ ( ♯ ‘ 𝐶 ) = 2 )
11	10	intnand	⊢ ( 𝐶 = { 𝑣 } → ¬ ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) )
12	1	eleq2i	⊢ ( 𝐶 ∈ 𝐸 ↔ 𝐶 ∈ ( Edg ‘ 𝐺 ) )
13		edgumgr	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) )
14	12 13	sylan2b	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸 ) → ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) )
15	11 14	nsyl3	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸 ) → ¬ 𝐶 = { 𝑣 } )
16	15	nexdv	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸 ) → ¬ ∃ 𝑣 𝐶 = { 𝑣 } )