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

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 ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐸 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) )