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

Metamath Proof Explorer

Theorem dfclnbgr4

Description: Alternate definition of the closed neighborhood of a vertex as union of the vertex with its open neighborhood. (Contributed by AV, 8-May-2025)

Ref Expression
Hypothesis dfclnbgr4.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion dfclnbgr4 ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 dfclnbgr4.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 dfclnbgr2 ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) )
4 undif2 ⊢ ( { 𝑁 } ∪ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
5 rabdif ⊢ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) }
6 5 uneq2i ⊢ ( { 𝑁 } ∪ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) ) = ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
7 4 6 eqtr3i ⊢ ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) = ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
8 1 2 dfnbgr2 ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
9 8 eqcomd ⊢ ( 𝑁 ∈ 𝑉 → { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } = ( 𝐺 NeighbVtx 𝑁 ) )
10 9 uneq2d ⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
11 7 10 eqtrid ⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
12 3 11 eqtrd ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )