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

Metamath Proof Explorer

Theorem clnbupgr

Description: The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025)

Ref Expression
Hypotheses clnbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clnbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion clnbupgr ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )

Proof

Step Hyp Ref Expression
1 clnbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 clnbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 dfclnbgr4 ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
4 3 adantl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
5 1 2 nbupgr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
6 5 uneq2d ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) = ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )
7 rabdif ⊢ ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ∖ { 𝑁 } ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 }
8 7 eqcomi ⊢ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } = ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ∖ { 𝑁 } )
9 8 uneq2i ⊢ ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) = ( { 𝑁 } ∪ ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ∖ { 𝑁 } ) )
10 undif2 ⊢ ( { 𝑁 } ∪ ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ∖ { 𝑁 } ) ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
11 9 10 eqtri ⊢ ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
12 11 a1i ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )
13 4 6 12 3eqtrd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )