Metamath Proof Explorer

Theorem umgredg

Description: For each edge in a multigraph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 25-Nov-2020)

Ref Expression
Hypotheses upgredg.v ⊢V=Vtx⁡G
upgredg.e ⊢E=Edg⁡G
Assertion umgredg ⊢G∈UMGraph∧C∈E→∃a∈V∃b∈Va≠b∧C=ab

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢V=Vtx⁡G
2 upgredg.e ⊢E=Edg⁡G
3 2 eleq2i ⊢C∈E↔C∈Edg⁡G
4 edgumgr ⊢G∈UMGraph∧C∈Edg⁡G→C∈𝒫Vtx⁡G∧C=2
5 3 4 sylan2b ⊢G∈UMGraph∧C∈E→C∈𝒫Vtx⁡G∧C=2
6 hash2prde ⊢C∈𝒫Vtx⁡G∧C=2→∃a∃ba≠b∧C=ab
7 eleq1 ⊢C=ab→C∈𝒫Vtx⁡G↔ab∈𝒫Vtx⁡G
8 prex ⊢ab∈V
9 8 elpw ⊢ab∈𝒫Vtx⁡G↔ab⊆Vtx⁡G
10 vex ⊢a∈V
11 vex ⊢b∈V
12 10 11 prss ⊢a∈V∧b∈V↔ab⊆V
13 1 sseq2i ⊢ab⊆V↔ab⊆Vtx⁡G
14 12 13 sylbbr ⊢ab⊆Vtx⁡G→a∈V∧b∈V
15 9 14 sylbi ⊢ab∈𝒫Vtx⁡G→a∈V∧b∈V
16 7 15 syl6bi ⊢C=ab→C∈𝒫Vtx⁡G→a∈V∧b∈V
17 16 adantrd ⊢C=ab→C∈𝒫Vtx⁡G∧C=2→a∈V∧b∈V
18 17 adantl ⊢a≠b∧C=ab→C∈𝒫Vtx⁡G∧C=2→a∈V∧b∈V
19 18 imdistanri ⊢C∈𝒫Vtx⁡G∧C=2∧a≠b∧C=ab→a∈V∧b∈V∧a≠b∧C=ab
20 19 ex ⊢C∈𝒫Vtx⁡G∧C=2→a≠b∧C=ab→a∈V∧b∈V∧a≠b∧C=ab
21 20 2eximdv ⊢C∈𝒫Vtx⁡G∧C=2→∃a∃ba≠b∧C=ab→∃a∃ba∈V∧b∈V∧a≠b∧C=ab
22 6 21 mpd ⊢C∈𝒫Vtx⁡G∧C=2→∃a∃ba∈V∧b∈V∧a≠b∧C=ab
23 5 22 syl ⊢G∈UMGraph∧C∈E→∃a∃ba∈V∧b∈V∧a≠b∧C=ab
24 r2ex ⊢∃a∈V∃b∈Va≠b∧C=ab↔∃a∃ba∈V∧b∈V∧a≠b∧C=ab
25 23 24 sylibr ⊢G∈UMGraph∧C∈E→∃a∈V∃b∈Va≠b∧C=ab