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 ⊢ E = Edg ⁡ G
Assertion umgrvad2edg ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ∃ x ∈ E ∃ y ∈ E x ≠ y ∧ N ∈ x ∧ N ∈ y

Proof

Step Hyp Ref Expression
1 umgrvad2edg.e ⊢ E = Edg ⁡ G
2 simpl ⊢ N A ∈ E ∧ B N ∈ E → N A ∈ E
3 simpr ⊢ N A ∈ E ∧ B N ∈ E → B N ∈ E
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 4 1 umgrpredgv ⊢ G ∈ UMGraph ∧ N A ∈ E → N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G
6 5 ex ⊢ G ∈ UMGraph → N A ∈ E → N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G
7 4 1 umgrpredgv ⊢ G ∈ UMGraph ∧ B N ∈ E → B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G
8 7 ex ⊢ G ∈ UMGraph → B N ∈ E → B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G
9 6 8 anim12d ⊢ G ∈ UMGraph → N A ∈ E ∧ B N ∈ E → N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G
10 9 adantr ⊢ G ∈ UMGraph ∧ A ≠ B → N A ∈ E ∧ B N ∈ E → N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G
11 10 imp ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G
12 simplr ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → A ≠ B
13 1 umgredgne ⊢ G ∈ UMGraph ∧ N A ∈ E → N ≠ A
14 13 necomd ⊢ G ∈ UMGraph ∧ N A ∈ E → A ≠ N
15 14 ad2ant2r ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → A ≠ N
16 12 15 jca ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → A ≠ B ∧ A ≠ N
17 16 olcd ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → N ≠ B ∧ N ≠ N ∨ A ≠ B ∧ A ≠ N
18 prneimg ⊢ N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G → N ≠ B ∧ N ≠ N ∨ A ≠ B ∧ A ≠ N → N A ≠ B N
19 18 imp ⊢ N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G ∧ N ≠ B ∧ N ≠ N ∨ A ≠ B ∧ A ≠ N → N A ≠ B N
20 prid1g ⊢ N ∈ Vtx ⁡ G → N ∈ N A
21 20 ad3antrrr ⊢ N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G ∧ N ≠ B ∧ N ≠ N ∨ A ≠ B ∧ A ≠ N → N ∈ N A
22 prid2g ⊢ N ∈ Vtx ⁡ G → N ∈ B N
23 22 ad3antrrr ⊢ N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G ∧ N ≠ B ∧ N ≠ N ∨ A ≠ B ∧ A ≠ N → N ∈ B N
24 19 21 23 3jca ⊢ N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G ∧ N ≠ B ∧ N ≠ N ∨ A ≠ B ∧ A ≠ N → N A ≠ B N ∧ N ∈ N A ∧ N ∈ B N
25 11 17 24 syl2anc ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → N A ≠ B N ∧ N ∈ N A ∧ N ∈ B N
26 neeq1 ⊢ x = N A → x ≠ y ↔ N A ≠ y
27 eleq2 ⊢ x = N A → N ∈ x ↔ N ∈ N A
28 26 27 3anbi12d ⊢ x = N A → x ≠ y ∧ N ∈ x ∧ N ∈ y ↔ N A ≠ y ∧ N ∈ N A ∧ N ∈ y
29 neeq2 ⊢ y = B N → N A ≠ y ↔ N A ≠ B N
30 eleq2 ⊢ y = B N → N ∈ y ↔ N ∈ B N
31 29 30 3anbi13d ⊢ y = B N → N A ≠ y ∧ N ∈ N A ∧ N ∈ y ↔ N A ≠ B N ∧ N ∈ N A ∧ N ∈ B N
32 28 31 rspc2ev ⊢ N A ∈ E ∧ B N ∈ E ∧ N A ≠ B N ∧ N ∈ N A ∧ N ∈ B N → ∃ x ∈ E ∃ y ∈ E x ≠ y ∧ N ∈ x ∧ N ∈ y
33 2 3 25 32 syl2an23an ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ∃ x ∈ E ∃ y ∈ E x ≠ y ∧ N ∈ x ∧ N ∈ y