Database
GRAPH THEORY
Undirected graphs
Undirected simple graphs
usgr2edg1
Metamath Proof Explorer
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