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 ⊢ I = iEdg ⁡ G
usgrf1oedg.e ⊢ E = Edg ⁡ G
Assertion umgr2edg ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ∃ x ∈ dom ⁡ I ∃ y ∈ dom ⁡ I x ≠ y ∧ N ∈ I ⁡ x ∧ N ∈ I ⁡ y

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i ⊢ I = iEdg ⁡ G
2 usgrf1oedg.e ⊢ E = Edg ⁡ G
3 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
4 3 anim1i ⊢ G ∈ UMGraph ∧ A ≠ B → G ∈ UHGraph ∧ A ≠ B
5 4 adantr ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → G ∈ UHGraph ∧ A ≠ B
6 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
7 6 2 umgrpredgv ⊢ G ∈ UMGraph ∧ N A ∈ E → N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G
8 7 ad2ant2r ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → N ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G
9 8 simprd ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → A ∈ Vtx ⁡ G
10 6 2 umgrpredgv ⊢ G ∈ UMGraph ∧ B N ∈ E → B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G
11 10 ad2ant2rl ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G
12 11 simpld ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → B ∈ Vtx ⁡ G
13 8 simpld ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → N ∈ Vtx ⁡ G
14 simpr ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → N A ∈ E ∧ B N ∈ E
15 1 2 6 uhgr2edg ⊢ G ∈ UHGraph ∧ A ≠ B ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G ∧ N A ∈ E ∧ B N ∈ E → ∃ x ∈ dom ⁡ I ∃ y ∈ dom ⁡ I x ≠ y ∧ N ∈ I ⁡ x ∧ N ∈ I ⁡ y
16 5 9 12 13 14 15 syl131anc ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ∃ x ∈ dom ⁡ I ∃ y ∈ dom ⁡ I x ≠ y ∧ N ∈ I ⁡ x ∧ N ∈ I ⁡ y