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	$⊢ N \in (G NeighbVtx K) \leftrightarrow K \in (G NeighbVtx N)$

Proof

Step	Hyp	Ref	Expression
1		ancom	$⊢ (N \in Vtx (G) \land K \in Vtx (G)) \leftrightarrow (K \in Vtx (G) \land N \in Vtx (G))$
2		necom	$⊢ N \neq K \leftrightarrow K \neq N$
3		prcom	$⊢ \{K, N\} = \{N, K\}$
4	3	sseq1i	$⊢ \{K, N\} \subseteq e \leftrightarrow \{N, K\} \subseteq e$
5	4	rexbii	$⊢ \exists e \in Edg (G) \{K, N\} \subseteq e \leftrightarrow \exists e \in Edg (G) \{N, K\} \subseteq e$
6	1 2 5	3anbi123i	$⊢ ((N \in Vtx (G) \land K \in Vtx (G)) \land N \neq K \land \exists e \in Edg (G) \{K, N\} \subseteq e) \leftrightarrow ((K \in Vtx (G) \land N \in Vtx (G)) \land K \neq N \land \exists e \in Edg (G) \{N, K\} \subseteq e)$
7		eqid	$⊢ Vtx (G) = Vtx (G)$
8		eqid	$⊢ Edg (G) = Edg (G)$
9	7 8	nbgrel	$⊢ N \in (G NeighbVtx K) \leftrightarrow ((N \in Vtx (G) \land K \in Vtx (G)) \land N \neq K \land \exists e \in Edg (G) \{K, N\} \subseteq e)$
10	7 8	nbgrel	$⊢ K \in (G NeighbVtx N) \leftrightarrow ((K \in Vtx (G) \land N \in Vtx (G)) \land K \neq N \land \exists e \in Edg (G) \{N, K\} \subseteq e)$
11	6 9 10	3bitr4i	$⊢ N \in (G NeighbVtx K) \leftrightarrow K \in (G NeighbVtx N)$

Metamath Proof Explorer

Theorem nbgrsym

Proof