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

Metamath Proof Explorer

Theorem nbgrsym

Description: In a graph, the 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 Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 27-Oct-2020) (Revised by AV, 12-Feb-2022)

Ref Expression
Assertion nbgrsym ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ 𝐾 ∈ ( 𝐺 NeighbVtx 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ancom ⊢ ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) ↔ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
2 necom ⊢ ( 𝑁 ≠ 𝐾 ↔ 𝐾 ≠ 𝑁 )
3 prcom ⊢ { 𝐾 , 𝑁 } = { 𝑁 , 𝐾 }
4 3 sseq1i ⊢ ( { 𝐾 , 𝑁 } ⊆ 𝑒 ↔ { 𝑁 , 𝐾 } ⊆ 𝑒 )
5 4 rexbii ⊢ ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 )
6 1 2 5 3anbi123i ⊢ ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑁 ≠ 𝐾 ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) ↔ ( ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝐾 ≠ 𝑁 ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 ) )
7 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
9 7 8 nbgrel ⊢ ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑁 ≠ 𝐾 ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) )
10 7 8 nbgrel ⊢ ( 𝐾 ∈ ( 𝐺 NeighbVtx 𝑁 ) ↔ ( ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝐾 ≠ 𝑁 ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 ) )
11 6 9 10 3bitr4i ⊢ ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ 𝐾 ∈ ( 𝐺 NeighbVtx 𝑁 ) )