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 ⊢ E = Edg ⁡ G
Assertion umgredgnlp ⊢ G ∈ UMGraph ∧ C ∈ E → ¬ ∃ v C = v

Proof

Step Hyp Ref Expression
1 umgredgnlp.e ⊢ E = Edg ⁡ G
2 vex ⊢ v ∈ V
3 hashsng ⊢ v ∈ 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 ∈ 𝒫 Vtx ⁡ G ∧ C = 2
12 1 eleq2i ⊢ C ∈ E ↔ C ∈ Edg ⁡ G
13 edgumgr ⊢ G ∈ UMGraph ∧ C ∈ Edg ⁡ G → C ∈ 𝒫 Vtx ⁡ G ∧ C = 2
14 12 13 sylan2b ⊢ G ∈ UMGraph ∧ C ∈ E → C ∈ 𝒫 Vtx ⁡ G ∧ C = 2
15 11 14 nsyl3 ⊢ G ∈ UMGraph ∧ C ∈ E → ¬ C = v
16 15 nexdv ⊢ G ∈ UMGraph ∧ C ∈ E → ¬ ∃ v C = v