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

Metamath Proof Explorer

Theorem clnbgrsym

Description: In a graph, the closed neighborhood relation is symmetric: a vertex N in a graph G is a neighbor of a second vertex K iff the second vertex K is a neighbor of the first vertex N . (Contributed by AV, 10-May-2025)

Ref Expression
Assertion clnbgrsym ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ 𝐾 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ancom ⊢ ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) ↔ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
2 eqcom ⊢ ( 𝑁 = 𝐾 ↔ 𝐾 = 𝑁 )
3 prcom ⊢ { 𝐾 , 𝑁 } = { 𝑁 , 𝐾 }
4 3 sseq1i ⊢ ( { 𝐾 , 𝑁 } ⊆ 𝑒 ↔ { 𝑁 , 𝐾 } ⊆ 𝑒 )
5 4 rexbii ⊢ ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 )
6 2 5 orbi12i ⊢ ( ( 𝑁 = 𝐾 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) ↔ ( 𝐾 = 𝑁 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 ) )
7 1 6 anbi12i ⊢ ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑁 = 𝐾 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) ) ↔ ( ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐾 = 𝑁 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 ) ) )
8 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
9 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
10 8 9 clnbgrel ⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑁 = 𝐾 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) ) )
11 8 9 clnbgrel ⊢ ( 𝐾 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) ↔ ( ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐾 = 𝑁 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 ) ) )
12 7 10 11 3bitr4i ⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ 𝐾 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) )