Theorem umgr2edgneu

Description: If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex, analogous to usgr2edg1 . Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 9-Jan-2020)

	Ref	Expression
Hypothesis	umgrvad2edg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	umgr2edgneu	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ 𝐸 𝑁 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		umgrvad2edg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2	1	umgrvad2edg	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐸 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) )
3		3simpc	⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) )
4		neneq	⊢ ( 𝑥 ≠ 𝑦 → ¬ 𝑥 = 𝑦 )
5	4	3ad2ant1	⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → ¬ 𝑥 = 𝑦 )
6	3 5	jca	⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
7	6	reximi	⊢ ( ∃ 𝑦 ∈ 𝐸 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → ∃ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
8	7	reximi	⊢ ( ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐸 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
9	2 8	syl	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
10		rexanali	⊢ ( ∃ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
11	10	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐸 ¬ ∀ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
12		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐸 ¬ ∀ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
13	11 12	bitri	⊢ ( ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
14	9 13	sylib	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∀ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
15	14	intnand	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ( ∃ 𝑥 ∈ 𝐸 𝑁 ∈ 𝑥 ∧ ∀ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )
16		eleq2w	⊢ ( 𝑥 = 𝑦 → ( 𝑁 ∈ 𝑥 ↔ 𝑁 ∈ 𝑦 ) )
17	16	reu4	⊢ ( ∃! 𝑥 ∈ 𝐸 𝑁 ∈ 𝑥 ↔ ( ∃ 𝑥 ∈ 𝐸 𝑁 ∈ 𝑥 ∧ ∀ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )
18	15 17	sylnibr	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ 𝐸 𝑁 ∈ 𝑥 )