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

Metamath Proof Explorer

Theorem umgr2edg

Description: If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 11-Feb-2021)

Ref Expression
Hypotheses usgrf1oedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
usgrf1oedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion umgr2edg ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 usgrf1oedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 umgruhgr ⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
4 3 anim1i ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) )
5 4 adantr ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) )
6 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
7 6 2 umgrpredgv ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝐴 } ∈ 𝐸 ) → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
8 7 ad2ant2r ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
9 8 simprd ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
10 6 2 umgrpredgv ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
11 10 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
12 11 simpld ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
13 8 simpld ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
14 simpr ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) )
15 1 2 6 uhgr2edg ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )
16 5 9 12 13 14 15 syl131anc ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )