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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
upgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion umgredg ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) )

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 upgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 2 eleq2i ⊢ ( 𝐶 ∈ 𝐸 ↔ 𝐶 ∈ ( Edg ‘ 𝐺 ) )
4 edgumgr ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) )
5 3 4 sylan2b ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸 ) → ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) )
6 hash2prde ⊢ ( ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) )
7 eleq1 ⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ { 𝑎 , 𝑏 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ) )
8 prex ⊢ { 𝑎 , 𝑏 } ∈ V
9 8 elpw ⊢ ( { 𝑎 , 𝑏 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) )
10 vex ⊢ 𝑎 ∈ V
11 vex ⊢ 𝑏 ∈ V
12 10 11 prss ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ↔ { 𝑎 , 𝑏 } ⊆ 𝑉 )
13 1 sseq2i ⊢ ( { 𝑎 , 𝑏 } ⊆ 𝑉 ↔ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) )
14 12 13 sylbbr ⊢ ( { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
15 9 14 sylbi ⊢ ( { 𝑎 , 𝑏 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
16 7 15 biimtrdi ⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
17 16 adantrd ⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
18 17 adantl ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) → ( ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
19 18 imdistanri ⊢ ( ( ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) ) )
20 19 ex ⊢ ( ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) ) ) )
21 20 2eximdv ⊢ ( ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) → ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) → ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) ) ) )
22 6 21 mpd ⊢ ( ( 𝐶 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐶 ) = 2 ) → ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) ) )
23 5 22 syl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸 ) → ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) ) )
24 r2ex ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) ) )
25 23 24 sylibr ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝐶 = { 𝑎 , 𝑏 } ) )