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

Proof

Step	Hyp	Ref	Expression
1		usgrf1oedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		usgrf1oedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		umgruhgr	⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
4	3	anim1i	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) )
5	4	adantr	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) )
6		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
7	6 2	umgrpredgv	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝐴 } ∈ 𝐸 ) → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
8	7	ad2ant2r	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
9	8	simprd	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
10	6 2	umgrpredgv	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
11	10	ad2ant2rl	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
12	11	simpld	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
13	8	simpld	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
14		simpr	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) )
15	1 2 6	uhgr2edg	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )
16	5 9 12 13 14 15	syl131anc	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )