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

Metamath Proof Explorer

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 ∧ 𝐶 ∈ 𝐸 ) → ¬ ∃ 𝑣 𝐶 = { 𝑣 } )