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∧NA∈E∧BN∈E→¬∃!x∈EN∈x

Proof

Step Hyp Ref Expression
1 umgrvad2edg.e ⊢E=Edg⁡G
2 1 umgrvad2edg ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→∃x∈E∃y∈Ex≠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∈Ex≠y∧N∈x∧N∈y→∃y∈EN∈x∧N∈y∧¬x=y
8 7 reximi ⊢∃x∈E∃y∈Ex≠y∧N∈x∧N∈y→∃x∈E∃y∈EN∈x∧N∈y∧¬x=y
9 2 8 syl ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→∃x∈E∃y∈EN∈x∧N∈y∧¬x=y
10 rexanali ⊢∃y∈EN∈x∧N∈y∧¬x=y↔¬∀y∈EN∈x∧N∈y→x=y
11 10 rexbii ⊢∃x∈E∃y∈EN∈x∧N∈y∧¬x=y↔∃x∈E¬∀y∈EN∈x∧N∈y→x=y
12 rexnal ⊢∃x∈E¬∀y∈EN∈x∧N∈y→x=y↔¬∀x∈E∀y∈EN∈x∧N∈y→x=y
13 11 12 bitri ⊢∃x∈E∃y∈EN∈x∧N∈y∧¬x=y↔¬∀x∈E∀y∈EN∈x∧N∈y→x=y
14 9 13 sylib ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→¬∀x∈E∀y∈EN∈x∧N∈y→x=y
15 14 intnand ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→¬∃x∈EN∈x∧∀x∈E∀y∈EN∈x∧N∈y→x=y
16 eleq2w ⊢x=y→N∈x↔N∈y
17 16 reu4 ⊢∃!x∈EN∈x↔∃x∈EN∈x∧∀x∈E∀y∈EN∈x∧N∈y→x=y
18 15 17 sylnibr ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→¬∃!x∈EN∈x