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 𝑁 ) )