Metamath Proof Explorer


Theorem usgr2edg1

Description: If a vertex is adjacent to two different vertices in a simple graph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 17-Oct-2020) (Proof shortened by AV, 8-Jun-2021)

Ref Expression
Hypotheses usgrf1oedg.i I = iEdg G
usgrf1oedg.e E = Edg G
Assertion usgr2edg1 G USGraph A B N A E B N E ¬ ∃! x dom I N I x

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i I = iEdg G
2 usgrf1oedg.e E = Edg G
3 usgrumgr G USGraph G UMGraph
4 1 2 umgr2edg1 G UMGraph A B N A E B N E ¬ ∃! x dom I N I x
5 3 4 sylanl1 G USGraph A B N A E B N E ¬ ∃! x dom I N I x