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 ∈ V a ≠ b ∧ C = a b

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 ∃ b a ≠ b ∧ C = a b
7 eleq1 ⊢ C = a b → C ∈ 𝒫 Vtx ⁡ G ↔ a b ∈ 𝒫 Vtx ⁡ G
8 prex ⊢ a b ∈ V
9 8 elpw ⊢ a b ∈ 𝒫 Vtx ⁡ G ↔ a b ⊆ Vtx ⁡ G
10 vex ⊢ a ∈ V
11 vex ⊢ b ∈ V
12 10 11 prss ⊢ a ∈ V ∧ b ∈ V ↔ a b ⊆ V
13 1 sseq2i ⊢ a b ⊆ V ↔ a b ⊆ Vtx ⁡ G
14 12 13 sylbbr ⊢ a b ⊆ Vtx ⁡ G → a ∈ V ∧ b ∈ V
15 9 14 sylbi ⊢ a b ∈ 𝒫 Vtx ⁡ G → a ∈ V ∧ b ∈ V
16 7 15 syl6bi ⊢ C = a b → C ∈ 𝒫 Vtx ⁡ G → a ∈ V ∧ b ∈ V
17 16 adantrd ⊢ C = a b → C ∈ 𝒫 Vtx ⁡ G ∧ C = 2 → a ∈ V ∧ b ∈ V
18 17 adantl ⊢ a ≠ b ∧ C = a b → C ∈ 𝒫 Vtx ⁡ G ∧ C = 2 → a ∈ V ∧ b ∈ V
19 18 imdistanri ⊢ C ∈ 𝒫 Vtx ⁡ G ∧ C = 2 ∧ a ≠ b ∧ C = a b → a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ C = a b
20 19 ex ⊢ C ∈ 𝒫 Vtx ⁡ G ∧ C = 2 → a ≠ b ∧ C = a b → a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ C = a b
21 20 2eximdv ⊢ C ∈ 𝒫 Vtx ⁡ G ∧ C = 2 → ∃ a ∃ b a ≠ b ∧ C = a b → ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ C = a b
22 6 21 mpd ⊢ C ∈ 𝒫 Vtx ⁡ G ∧ C = 2 → ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ C = a b
23 5 22 syl ⊢ G ∈ UMGraph ∧ C ∈ E → ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ C = a b
24 r2ex ⊢ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ C = a b ↔ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ C = a b
25 23 24 sylibr ⊢ G ∈ UMGraph ∧ C ∈ E → ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ C = a b