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∧NA∈E∧BN∈E→∃x∈dom⁡I∃y∈dom⁡Ix≠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∧NA∈E∧BN∈E→G∈UHGraph∧A≠B
6 eqid ⊢Vtx⁡G=Vtx⁡G
7 6 2 umgrpredgv ⊢G∈UMGraph∧NA∈E→N∈Vtx⁡G∧A∈Vtx⁡G
8 7 ad2ant2r ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→N∈Vtx⁡G∧A∈Vtx⁡G
9 8 simprd ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→A∈Vtx⁡G
10 6 2 umgrpredgv ⊢G∈UMGraph∧BN∈E→B∈Vtx⁡G∧N∈Vtx⁡G
11 10 ad2ant2rl ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→B∈Vtx⁡G∧N∈Vtx⁡G
12 11 simpld ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→B∈Vtx⁡G
13 8 simpld ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→N∈Vtx⁡G
14 simpr ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→NA∈E∧BN∈E
15 1 2 6 uhgr2edg ⊢G∈UHGraph∧A≠B∧A∈Vtx⁡G∧B∈Vtx⁡G∧N∈Vtx⁡G∧NA∈E∧BN∈E→∃x∈dom⁡I∃y∈dom⁡Ix≠y∧N∈I⁡x∧N∈I⁡y
16 5 9 12 13 14 15 syl131anc ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→∃x∈dom⁡I∃y∈dom⁡Ix≠y∧N∈I⁡x∧N∈I⁡y