Theorem umgr2edg1

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

	Ref	Expression
Hypotheses	usgrf1oedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	usgrf1oedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	umgr2edg1	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		usgrf1oedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		usgrf1oedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	umgr2edg	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )
4		3anrot	⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ↔ ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
5		df-ne	⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
6	5	3anbi3i	⊢ ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
7	4 6	bitri	⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ↔ ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
8		df-3an	⊢ ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) )
9	7 8	bitri	⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ↔ ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) )
10	9	2rexbii	⊢ ( ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) )
11	3 10	sylib	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) )
12		rexanali	⊢ ( ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
13	12	rexbii	⊢ ( ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ∈ dom 𝐼 ¬ ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
14		rexnal	⊢ ( ∃ 𝑥 ∈ dom 𝐼 ¬ ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
15	13 14	bitri	⊢ ( ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
16	11 15	sylib	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
17	16	intnand	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ( ∃ 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) )
18		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) )
19	18	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ↔ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )
20	19	reu4	⊢ ( ∃! 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ↔ ( ∃ 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) )
21	17 20	sylnibr	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) )