Metamath Proof Explorer

Theorem umgrvad2edg

Description: If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex, analogous to usgr2edg . (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 9-Jan-2020) (Revised by AV, 8-Jun-2021)

Ref Expression
Hypothesis umgrvad2edg.e ⊢E=Edg⁡G
Assertion umgrvad2edg ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→∃x∈E∃y∈Ex≠y∧N∈x∧N∈y

Proof

Step Hyp Ref Expression
1 umgrvad2edg.e ⊢E=Edg⁡G
2 simpl ⊢NA∈E∧BN∈E→NA∈E
3 simpr ⊢NA∈E∧BN∈E→BN∈E
4 eqid ⊢Vtx⁡G=Vtx⁡G
5 4 1 umgrpredgv ⊢G∈UMGraph∧NA∈E→N∈Vtx⁡G∧A∈Vtx⁡G
6 5 ex ⊢G∈UMGraph→NA∈E→N∈Vtx⁡G∧A∈Vtx⁡G
7 4 1 umgrpredgv ⊢G∈UMGraph∧BN∈E→B∈Vtx⁡G∧N∈Vtx⁡G
8 7 ex ⊢G∈UMGraph→BN∈E→B∈Vtx⁡G∧N∈Vtx⁡G
9 6 8 anim12d ⊢G∈UMGraph→NA∈E∧BN∈E→N∈Vtx⁡G∧A∈Vtx⁡G∧B∈Vtx⁡G∧N∈Vtx⁡G
10 9 adantr ⊢G∈UMGraph∧A≠B→NA∈E∧BN∈E→N∈Vtx⁡G∧A∈Vtx⁡G∧B∈Vtx⁡G∧N∈Vtx⁡G
11 10 imp ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→N∈Vtx⁡G∧A∈Vtx⁡G∧B∈Vtx⁡G∧N∈Vtx⁡G
12 simplr ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→A≠B
13 1 umgredgne ⊢G∈UMGraph∧NA∈E→N≠A
14 13 necomd ⊢G∈UMGraph∧NA∈E→A≠N
15 14 ad2ant2r ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→A≠N
16 12 15 jca ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→A≠B∧A≠N
17 16 olcd ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→N≠B∧N≠N∨A≠B∧A≠N
18 prneimg ⊢N∈Vtx⁡G∧A∈Vtx⁡G∧B∈Vtx⁡G∧N∈Vtx⁡G→N≠B∧N≠N∨A≠B∧A≠N→NA≠BN
19 18 imp ⊢N∈Vtx⁡G∧A∈Vtx⁡G∧B∈Vtx⁡G∧N∈Vtx⁡G∧N≠B∧N≠N∨A≠B∧A≠N→NA≠BN
20 prid1g ⊢N∈Vtx⁡G→N∈NA
21 20 ad3antrrr ⊢N∈Vtx⁡G∧A∈Vtx⁡G∧B∈Vtx⁡G∧N∈Vtx⁡G∧N≠B∧N≠N∨A≠B∧A≠N→N∈NA
22 prid2g ⊢N∈Vtx⁡G→N∈BN
23 22 ad3antrrr ⊢N∈Vtx⁡G∧A∈Vtx⁡G∧B∈Vtx⁡G∧N∈Vtx⁡G∧N≠B∧N≠N∨A≠B∧A≠N→N∈BN
24 19 21 23 3jca ⊢N∈Vtx⁡G∧A∈Vtx⁡G∧B∈Vtx⁡G∧N∈Vtx⁡G∧N≠B∧N≠N∨A≠B∧A≠N→NA≠BN∧N∈NA∧N∈BN
25 11 17 24 syl2anc ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→NA≠BN∧N∈NA∧N∈BN
26 neeq1 ⊢x=NA→x≠y↔NA≠y
27 eleq2 ⊢x=NA→N∈x↔N∈NA
28 26 27 3anbi12d ⊢x=NA→x≠y∧N∈x∧N∈y↔NA≠y∧N∈NA∧N∈y
29 neeq2 ⊢y=BN→NA≠y↔NA≠BN
30 eleq2 ⊢y=BN→N∈y↔N∈BN
31 29 30 3anbi13d ⊢y=BN→NA≠y∧N∈NA∧N∈y↔NA≠BN∧N∈NA∧N∈BN
32 28 31 rspc2ev ⊢NA∈E∧BN∈E∧NA≠BN∧N∈NA∧N∈BN→∃x∈E∃y∈Ex≠y∧N∈x∧N∈y
33 2 3 25 32 syl2an23an ⊢G∈UMGraph∧A≠B∧NA∈E∧BN∈E→∃x∈E∃y∈Ex≠y∧N∈x∧N∈y