This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nbumgr

Description: The set of neighbors of an arbitrary class in a multigraph. (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbumgr ( 𝐺 ∈ UMGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 nbumgrvtx ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
4 3 expcom ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ UMGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )
5 df-nel ⊢ ( 𝑁 ∉ 𝑉 ↔ ¬ 𝑁 ∈ 𝑉 )
6 1 nbgrnvtx0 ⊢ ( 𝑁 ∉ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
7 5 6 sylbir ⊢ ( ¬ 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
8 7 adantr ⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
9 1 2 umgrpredgv ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝑛 } ∈ 𝐸 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) )
10 9 simpld ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝑛 } ∈ 𝐸 ) → 𝑁 ∈ 𝑉 )
11 10 ex ⊢ ( 𝐺 ∈ UMGraph → ( { 𝑁 , 𝑛 } ∈ 𝐸 → 𝑁 ∈ 𝑉 ) )
12 11 adantl ⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( { 𝑁 , 𝑛 } ∈ 𝐸 → 𝑁 ∈ 𝑉 ) )
13 12 con3d ⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( ¬ 𝑁 ∈ 𝑉 → ¬ { 𝑁 , 𝑛 } ∈ 𝐸 ) )
14 13 ex ⊢ ( 𝑛 ∈ 𝑉 → ( 𝐺 ∈ UMGraph → ( ¬ 𝑁 ∈ 𝑉 → ¬ { 𝑁 , 𝑛 } ∈ 𝐸 ) ) )
15 14 com13 ⊢ ( ¬ 𝑁 ∈ 𝑉 → ( 𝐺 ∈ UMGraph → ( 𝑛 ∈ 𝑉 → ¬ { 𝑁 , 𝑛 } ∈ 𝐸 ) ) )
16 15 imp ⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( 𝑛 ∈ 𝑉 → ¬ { 𝑁 , 𝑛 } ∈ 𝐸 ) )
17 16 ralrimiv ⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ∀ 𝑛 ∈ 𝑉 ¬ { 𝑁 , 𝑛 } ∈ 𝐸 )
18 rabeq0 ⊢ ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } = ∅ ↔ ∀ 𝑛 ∈ 𝑉 ¬ { 𝑁 , 𝑛 } ∈ 𝐸 )
19 17 18 sylibr ⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } = ∅ )
20 8 19 eqtr4d ⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
21 20 ex ⊢ ( ¬ 𝑁 ∈ 𝑉 → ( 𝐺 ∈ UMGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )
22 4 21 pm2.61i ⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )