# 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 𝐼 ( 𝑥𝑦𝑁 ∈ ( 𝐼𝑥 ) ∧ 𝑁 ∈ ( 𝐼𝑦 ) ) )