This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐸 = ( 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 ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ 𝐸 𝑁 ∈ 𝑥 )