Metamath Proof Explorer

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 ⊢ E = Edg ⁡ G
Assertion umgr2edgneu ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ¬ ∃! x ∈ E N ∈ x

Proof

Step Hyp Ref Expression
1 umgrvad2edg.e ⊢ E = Edg ⁡ G
2 1 umgrvad2edg ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ∃ x ∈ E ∃ y ∈ E x ≠ y ∧ N ∈ x ∧ N ∈ y
3 3simpc ⊢ x ≠ y ∧ N ∈ x ∧ N ∈ y → N ∈ x ∧ N ∈ y
4 neneq ⊢ x ≠ y → ¬ x = y
5 4 3ad2ant1 ⊢ x ≠ y ∧ N ∈ x ∧ N ∈ y → ¬ x = y
6 3 5 jca ⊢ x ≠ y ∧ N ∈ x ∧ N ∈ y → N ∈ x ∧ N ∈ y ∧ ¬ x = y
7 6 reximi ⊢ ∃ y ∈ E x ≠ y ∧ N ∈ x ∧ N ∈ y → ∃ y ∈ E N ∈ x ∧ N ∈ y ∧ ¬ x = y
8 7 reximi ⊢ ∃ x ∈ E ∃ y ∈ E x ≠ y ∧ N ∈ x ∧ N ∈ y → ∃ x ∈ E ∃ y ∈ E N ∈ x ∧ N ∈ y ∧ ¬ x = y
9 2 8 syl ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ∃ x ∈ E ∃ y ∈ E N ∈ x ∧ N ∈ y ∧ ¬ x = y
10 rexanali ⊢ ∃ y ∈ E N ∈ x ∧ N ∈ y ∧ ¬ x = y ↔ ¬ ∀ y ∈ E N ∈ x ∧ N ∈ y → x = y
11 10 rexbii ⊢ ∃ x ∈ E ∃ y ∈ E N ∈ x ∧ N ∈ y ∧ ¬ x = y ↔ ∃ x ∈ E ¬ ∀ y ∈ E N ∈ x ∧ N ∈ y → x = y
12 rexnal ⊢ ∃ x ∈ E ¬ ∀ y ∈ E N ∈ x ∧ N ∈ y → x = y ↔ ¬ ∀ x ∈ E ∀ y ∈ E N ∈ x ∧ N ∈ y → x = y
13 11 12 bitri ⊢ ∃ x ∈ E ∃ y ∈ E N ∈ x ∧ N ∈ y ∧ ¬ x = y ↔ ¬ ∀ x ∈ E ∀ y ∈ E N ∈ x ∧ N ∈ y → x = y
14 9 13 sylib ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ¬ ∀ x ∈ E ∀ y ∈ E N ∈ x ∧ N ∈ y → x = y
15 14 intnand ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ¬ ∃ x ∈ E N ∈ x ∧ ∀ x ∈ E ∀ y ∈ E N ∈ x ∧ N ∈ y → x = y
16 eleq2w ⊢ x = y → N ∈ x ↔ N ∈ y
17 16 reu4 ⊢ ∃! x ∈ E N ∈ x ↔ ∃ x ∈ E N ∈ x ∧ ∀ x ∈ E ∀ y ∈ E N ∈ x ∧ N ∈ y → x = y
18 15 17 sylnibr ⊢ G ∈ UMGraph ∧ A ≠ B ∧ N A ∈ E ∧ B N ∈ E → ¬ ∃! x ∈ E N ∈ x