Theorem nbusgrf1o

Description: The set of neighbors of a vertex is isomorphic to the set of edges containing the vertex in a simple graph. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 28-Oct-2020)

	Ref	Expression
Hypotheses	nbusgrf1o.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	nbusgrf1o.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	nbusgrf1o	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \exists ff:G\mathrm{NeighbVtx}U\underset{1-1\; onto}{⟶}\left\{e\in E|U\in e\right\}$$

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		nbusgrf1o.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		eqid	$$⊢G\mathrm{NeighbVtx}U=G\mathrm{NeighbVtx}U$$
4		eleq2w	$$⊢e=c\to \left(U\in e\leftrightarrow U\in c\right)$$
5	4	cbvrabv	$$⊢\left\{e\in E|U\in e\right\}=\left\{c\in E|U\in c\right\}$$
6	1 2 3 5	nbusgrf1o1	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \exists ff:G\mathrm{NeighbVtx}U\underset{1-1\; onto}{⟶}\left\{e\in E|U\in e\right\}$$