Metamath Proof Explorer

Theorem umgr2v2enb1

Description: In a multigraph with two edges connecting the same two vertices, each of the vertices has one neighbor. (Contributed by AV, 18-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g ⊢G=V0AB1AB
Assertion umgr2v2enb1 ⊢V∈W∧A∈V∧B∈V∧A≠B→GNeighbVtxA=B

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g ⊢G=V0AB1AB
2 1 umgr2v2e ⊢V∈W∧A∈V∧B∈V∧A≠B→G∈UMGraph
3 1 umgr2v2evtxel ⊢V∈W∧A∈V→A∈Vtx⁡G
4 3 3adant3 ⊢V∈W∧A∈V∧B∈V→A∈Vtx⁡G
5 4 adantr ⊢V∈W∧A∈V∧B∈V∧A≠B→A∈Vtx⁡G
6 eqid ⊢Vtx⁡G=Vtx⁡G
7 eqid ⊢Edg⁡G=Edg⁡G
8 6 7 nbumgrvtx ⊢G∈UMGraph∧A∈Vtx⁡G→GNeighbVtxA=x∈Vtx⁡G|Ax∈Edg⁡G
9 2 5 8 syl2anc ⊢V∈W∧A∈V∧B∈V∧A≠B→GNeighbVtxA=x∈Vtx⁡G|Ax∈Edg⁡G
10 1 umgr2v2eedg ⊢V∈W∧A∈V∧B∈V→Edg⁡G=AB
11 10 eleq2d ⊢V∈W∧A∈V∧B∈V→Ax∈Edg⁡G↔Ax∈AB
12 11 adantr ⊢V∈W∧A∈V∧B∈V∧A≠B→Ax∈Edg⁡G↔Ax∈AB
13 12 adantr ⊢V∈W∧A∈V∧B∈V∧A≠B∧x∈Vtx⁡G→Ax∈Edg⁡G↔Ax∈AB
14 prex ⊢Ax∈V
15 14 elsn ⊢Ax∈AB↔Ax=AB
16 13 15 bitrdi ⊢V∈W∧A∈V∧B∈V∧A≠B∧x∈Vtx⁡G→Ax∈Edg⁡G↔Ax=AB
17 simpr ⊢V∈W∧A∈V∧B∈V∧A≠B∧x∈Vtx⁡G→x∈Vtx⁡G
18 simpll3 ⊢V∈W∧A∈V∧B∈V∧A≠B∧x∈Vtx⁡G→B∈V
19 17 18 preq2b ⊢V∈W∧A∈V∧B∈V∧A≠B∧x∈Vtx⁡G→Ax=AB↔x=B
20 16 19 bitrd ⊢V∈W∧A∈V∧B∈V∧A≠B∧x∈Vtx⁡G→Ax∈Edg⁡G↔x=B
21 20 pm5.32da ⊢V∈W∧A∈V∧B∈V∧A≠B→x∈Vtx⁡G∧Ax∈Edg⁡G↔x∈Vtx⁡G∧x=B
22 1 umgr2v2evtx ⊢V∈W→Vtx⁡G=V
23 22 3ad2ant1 ⊢V∈W∧A∈V∧B∈V→Vtx⁡G=V
24 eleq12 ⊢x=B∧Vtx⁡G=V→x∈Vtx⁡G↔B∈V
25 24 exbiri ⊢x=B→Vtx⁡G=V→B∈V→x∈Vtx⁡G
26 25 com13 ⊢B∈V→Vtx⁡G=V→x=B→x∈Vtx⁡G
27 26 3ad2ant3 ⊢V∈W∧A∈V∧B∈V→Vtx⁡G=V→x=B→x∈Vtx⁡G
28 23 27 mpd ⊢V∈W∧A∈V∧B∈V→x=B→x∈Vtx⁡G
29 28 adantr ⊢V∈W∧A∈V∧B∈V∧A≠B→x=B→x∈Vtx⁡G
30 29 pm4.71rd ⊢V∈W∧A∈V∧B∈V∧A≠B→x=B↔x∈Vtx⁡G∧x=B
31 21 30 bitr4d ⊢V∈W∧A∈V∧B∈V∧A≠B→x∈Vtx⁡G∧Ax∈Edg⁡G↔x=B
32 31 alrimiv ⊢V∈W∧A∈V∧B∈V∧A≠B→∀xx∈Vtx⁡G∧Ax∈Edg⁡G↔x=B
33 rabeqsn ⊢x∈Vtx⁡G|Ax∈Edg⁡G=B↔∀xx∈Vtx⁡G∧Ax∈Edg⁡G↔x=B
34 32 33 sylibr ⊢V∈W∧A∈V∧B∈V∧A≠B→x∈Vtx⁡G|Ax∈Edg⁡G=B
35 9 34 eqtrd ⊢V∈W∧A∈V∧B∈V∧A≠B→GNeighbVtxA=B