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