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	Could not format assertion : No typesetting found for |- ( N e. ( G ClNeighbVtx K ) <-> K e. ( G ClNeighbVtx N ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ancom	$$⊢\left(N\in \mathrm{Vtx}\left(G\right)\wedge K\in \mathrm{Vtx}\left(G\right)\right)\leftrightarrow \left(K\in \mathrm{Vtx}\left(G\right)\wedge N\in \mathrm{Vtx}\left(G\right)\right)$$
2		eqcom	$$⊢N=K\leftrightarrow K=N$$
3		prcom	$$⊢\left\{K,N\right\}=\left\{N,K\right\}$$
4	3	sseq1i	$$⊢\left\{K,N\right\}\subseteq e\leftrightarrow \left\{N,K\right\}\subseteq e$$
5	4	rexbii	$$⊢\exists e\in \mathrm{Edg}\left(G\right)\left\{K,N\right\}\subseteq e\leftrightarrow \exists e\in \mathrm{Edg}\left(G\right)\left\{N,K\right\}\subseteq e$$
6	2 5	orbi12i	$$⊢\left(N=K\vee \exists e\in \mathrm{Edg}\left(G\right)\left\{K,N\right\}\subseteq e\right)\leftrightarrow \left(K=N\vee \exists e\in \mathrm{Edg}\left(G\right)\left\{N,K\right\}\subseteq e\right)$$
7	1 6	anbi12i	$$⊢\left(\left(N\in \mathrm{Vtx}\left(G\right)\wedge K\in \mathrm{Vtx}\left(G\right)\right)\wedge \left(N=K\vee \exists e\in \mathrm{Edg}\left(G\right)\left\{K,N\right\}\subseteq e\right)\right)\leftrightarrow \left(\left(K\in \mathrm{Vtx}\left(G\right)\wedge N\in \mathrm{Vtx}\left(G\right)\right)\wedge \left(K=N\vee \exists e\in \mathrm{Edg}\left(G\right)\left\{N,K\right\}\subseteq e\right)\right)$$
8		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
9		eqid	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{Edg}\left(G\right)$$
10	8 9	clnbgrel	Could not format ( N e. ( G ClNeighbVtx K ) <-> ( ( N e. ( Vtx ` G ) /\ K e. ( Vtx ` G ) ) /\ ( N = K \/ E. e e. ( Edg ` G ) { K , N } C_ e ) ) ) : No typesetting found for |- ( N e. ( G ClNeighbVtx K ) <-> ( ( N e. ( Vtx ` G ) /\ K e. ( Vtx ` G ) ) /\ ( N = K \/ E. e e. ( Edg ` G ) { K , N } C_ e ) ) ) with typecode |-
11	8 9	clnbgrel	Could not format ( K e. ( G ClNeighbVtx N ) <-> ( ( K e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) /\ ( K = N \/ E. e e. ( Edg ` G ) { N , K } C_ e ) ) ) : No typesetting found for |- ( K e. ( G ClNeighbVtx N ) <-> ( ( K e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) /\ ( K = N \/ E. e e. ( Edg ` G ) { N , K } C_ e ) ) ) with typecode |-
12	7 10 11	3bitr4i	Could not format ( N e. ( G ClNeighbVtx K ) <-> K e. ( G ClNeighbVtx N ) ) : No typesetting found for |- ( N e. ( G ClNeighbVtx K ) <-> K e. ( G ClNeighbVtx N ) ) with typecode |-