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	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	usgrf1oedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	usgr2edg1	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		usgrf1oedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		usgrf1oedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
4	1 2	umgr2edg1	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) )
5	3 4	sylanl1	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) )