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 ⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
Assertion umgr2v2enb1 ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 } )

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g ⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
2 1 umgr2v2e ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐺 ∈ UMGraph )
3 1 umgr2v2evtxel ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
4 3 3adant3 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
5 4 adantr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
6 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
7 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
8 6 7 nbumgrvtx ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 NeighbVtx 𝐴 ) = { 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) } )
9 2 5 8 syl2anc ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐺 NeighbVtx 𝐴 ) = { 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) } )
10 1 umgr2v2eedg ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( Edg ‘ 𝐺 ) = { { 𝐴 , 𝐵 } } )
11 10 eleq2d ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐴 , 𝑥 } ∈ { { 𝐴 , 𝐵 } } ) )
12 11 adantr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐴 , 𝑥 } ∈ { { 𝐴 , 𝐵 } } ) )
13 12 adantr ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) → ( { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐴 , 𝑥 } ∈ { { 𝐴 , 𝐵 } } ) )
14 prex ⊢ { 𝐴 , 𝑥 } ∈ V
15 14 elsn ⊢ ( { 𝐴 , 𝑥 } ∈ { { 𝐴 , 𝐵 } } ↔ { 𝐴 , 𝑥 } = { 𝐴 , 𝐵 } )
16 13 15 bitrdi ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) → ( { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐴 , 𝑥 } = { 𝐴 , 𝐵 } ) )
17 simpr ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑥 ∈ ( Vtx ‘ 𝐺 ) )
18 simpll3 ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) → 𝐵 ∈ 𝑉 )
19 17 18 preq2b ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) → ( { 𝐴 , 𝑥 } = { 𝐴 , 𝐵 } ↔ 𝑥 = 𝐵 ) )
20 16 19 bitrd ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) → ( { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ↔ 𝑥 = 𝐵 ) )
21 20 pm5.32da ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑥 = 𝐵 ) ) )
22 1 umgr2v2evtx ⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )
23 22 3ad2ant1 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( Vtx ‘ 𝐺 ) = 𝑉 )
24 eleq12 ⊢ ( ( 𝑥 = 𝐵 ∧ ( Vtx ‘ 𝐺 ) = 𝑉 ) → ( 𝑥 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐵 ∈ 𝑉 ) )
25 24 exbiri ⊢ ( 𝑥 = 𝐵 → ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( 𝐵 ∈ 𝑉 → 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) ) )
26 25 com13 ⊢ ( 𝐵 ∈ 𝑉 → ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( 𝑥 = 𝐵 → 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) ) )
27 26 3ad2ant3 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( 𝑥 = 𝐵 → 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) ) )
28 23 27 mpd ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑥 = 𝐵 → 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) )
29 28 adantr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑥 = 𝐵 → 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) )
30 29 pm4.71rd ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑥 = 𝐵 ↔ ( 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑥 = 𝐵 ) ) )
31 21 30 bitr4d ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ) ↔ 𝑥 = 𝐵 ) )
32 31 alrimiv ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑥 ( ( 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ) ↔ 𝑥 = 𝐵 ) )
33 rabeqsn ⊢ ( { 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) } = { 𝐵 } ↔ ∀ 𝑥 ( ( 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ) ↔ 𝑥 = 𝐵 ) )
34 32 33 sylibr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐴 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) } = { 𝐵 } )
35 9 34 eqtrd ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 } )