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 = V 0 A B 1 A B
Assertion umgr2v2enb1 ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → G NeighbVtx A = B

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g ⊢ G = V 0 A B 1 A B
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 → G NeighbVtx A = x ∈ Vtx ⁡ G | A x ∈ Edg ⁡ G
9 2 5 8 syl2anc ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → G NeighbVtx A = x ∈ Vtx ⁡ G | A x ∈ Edg ⁡ G
10 1 umgr2v2eedg ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → Edg ⁡ G = A B
11 10 eleq2d ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → A x ∈ Edg ⁡ G ↔ A x ∈ A B
12 11 adantr ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A x ∈ Edg ⁡ G ↔ A x ∈ A B
13 12 adantr ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ x ∈ Vtx ⁡ G → A x ∈ Edg ⁡ G ↔ A x ∈ A B
14 prex ⊢ A x ∈ V
15 14 elsn ⊢ A x ∈ A B ↔ A x = A B
16 13 15 bitrdi ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ x ∈ Vtx ⁡ G → A x ∈ Edg ⁡ G ↔ A x = A B
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 → A x = A B ↔ x = B
20 16 19 bitrd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ x ∈ Vtx ⁡ G → A x ∈ Edg ⁡ G ↔ x = B
21 20 pm5.32da ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → x ∈ Vtx ⁡ G ∧ A x ∈ 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 ∧ A x ∈ Edg ⁡ G ↔ x = B
32 31 alrimiv ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → ∀ x x ∈ Vtx ⁡ G ∧ A x ∈ Edg ⁡ G ↔ x = B
33 rabeqsn ⊢ x ∈ Vtx ⁡ G | A x ∈ Edg ⁡ G = B ↔ ∀ x x ∈ Vtx ⁡ G ∧ A x ∈ Edg ⁡ G ↔ x = B
34 32 33 sylibr ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → x ∈ Vtx ⁡ G | A x ∈ Edg ⁡ G = B
35 9 34 eqtrd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → G NeighbVtx A = B