Metamath Proof Explorer


Theorem umgrvad2edg

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

Ref Expression
Hypothesis umgrvad2edg.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion umgrvad2edg ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥𝐸𝑦𝐸 ( 𝑥𝑦𝑁𝑥𝑁𝑦 ) )

Proof

Step Hyp Ref Expression
1 umgrvad2edg.e 𝐸 = ( Edg ‘ 𝐺 )
2 simpl ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → { 𝑁 , 𝐴 } ∈ 𝐸 )
3 simpr ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → { 𝐵 , 𝑁 } ∈ 𝐸 )
4 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 4 1 umgrpredgv ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝐴 } ∈ 𝐸 ) → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
6 5 ex ( 𝐺 ∈ UMGraph → ( { 𝑁 , 𝐴 } ∈ 𝐸 → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) )
7 4 1 umgrpredgv ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
8 7 ex ( 𝐺 ∈ UMGraph → ( { 𝐵 , 𝑁 } ∈ 𝐸 → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) )
9 6 8 anim12d ( 𝐺 ∈ UMGraph → ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ) )
10 9 adantr ( ( 𝐺 ∈ UMGraph ∧ 𝐴𝐵 ) → ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ) )
11 10 imp ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) )
12 simplr ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐴𝐵 )
13 1 umgredgne ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝐴 } ∈ 𝐸 ) → 𝑁𝐴 )
14 13 necomd ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝐴 } ∈ 𝐸 ) → 𝐴𝑁 )
15 14 ad2ant2r ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐴𝑁 )
16 12 15 jca ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( 𝐴𝐵𝐴𝑁 ) )
17 16 olcd ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( ( 𝑁𝐵𝑁𝑁 ) ∨ ( 𝐴𝐵𝐴𝑁 ) ) )
18 prneimg ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝑁𝐵𝑁𝑁 ) ∨ ( 𝐴𝐵𝐴𝑁 ) ) → { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ) )
19 18 imp ( ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑁𝐵𝑁𝑁 ) ∨ ( 𝐴𝐵𝐴𝑁 ) ) ) → { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } )
20 prid1g ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) → 𝑁 ∈ { 𝑁 , 𝐴 } )
21 20 ad3antrrr ( ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑁𝐵𝑁𝑁 ) ∨ ( 𝐴𝐵𝐴𝑁 ) ) ) → 𝑁 ∈ { 𝑁 , 𝐴 } )
22 prid2g ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) → 𝑁 ∈ { 𝐵 , 𝑁 } )
23 22 ad3antrrr ( ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑁𝐵𝑁𝑁 ) ∨ ( 𝐴𝐵𝐴𝑁 ) ) ) → 𝑁 ∈ { 𝐵 , 𝑁 } )
24 19 21 23 3jca ( ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑁𝐵𝑁𝑁 ) ∨ ( 𝐴𝐵𝐴𝑁 ) ) ) → ( { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ { 𝐵 , 𝑁 } ) )
25 11 17 24 syl2anc ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ { 𝐵 , 𝑁 } ) )
26 neeq1 ( 𝑥 = { 𝑁 , 𝐴 } → ( 𝑥𝑦 ↔ { 𝑁 , 𝐴 } ≠ 𝑦 ) )
27 eleq2 ( 𝑥 = { 𝑁 , 𝐴 } → ( 𝑁𝑥𝑁 ∈ { 𝑁 , 𝐴 } ) )
28 26 27 3anbi12d ( 𝑥 = { 𝑁 , 𝐴 } → ( ( 𝑥𝑦𝑁𝑥𝑁𝑦 ) ↔ ( { 𝑁 , 𝐴 } ≠ 𝑦𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁𝑦 ) ) )
29 neeq2 ( 𝑦 = { 𝐵 , 𝑁 } → ( { 𝑁 , 𝐴 } ≠ 𝑦 ↔ { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ) )
30 eleq2 ( 𝑦 = { 𝐵 , 𝑁 } → ( 𝑁𝑦𝑁 ∈ { 𝐵 , 𝑁 } ) )
31 29 30 3anbi13d ( 𝑦 = { 𝐵 , 𝑁 } → ( ( { 𝑁 , 𝐴 } ≠ 𝑦𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁𝑦 ) ↔ ( { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ { 𝐵 , 𝑁 } ) ) )
32 28 31 rspc2ev ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ∧ ( { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ { 𝐵 , 𝑁 } ) ) → ∃ 𝑥𝐸𝑦𝐸 ( 𝑥𝑦𝑁𝑥𝑁𝑦 ) )
33 2 3 25 32 syl2an23an ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥𝐸𝑦𝐸 ( 𝑥𝑦𝑁𝑥𝑁𝑦 ) )