Theorem nbusgrf1o1

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	nbusgrf1o1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	nbusgrf1o1.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
	nbusgrf1o1.n	$$⊢N=G\mathrm{NeighbVtx}U$$
	nbusgrf1o1.i	$$⊢I=\left\{e\in E|U\in e\right\}$$
Assertion	nbusgrf1o1	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \exists ff:N\underset{1-1\; onto}{⟶}I$$

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		nbusgrf1o1.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		nbusgrf1o1.n	$$⊢N=G\mathrm{NeighbVtx}U$$
4		nbusgrf1o1.i	$$⊢I=\left\{e\in E|U\in e\right\}$$
5	3	ovexi	$$⊢N\in \mathrm{V}$$
6		mptexg	$$⊢N\in \mathrm{V}\to \left(n\in N⟼\left\{U,n\right\}\right)\in \mathrm{V}$$
7	5 6	mp1i	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \left(n\in N⟼\left\{U,n\right\}\right)\in \mathrm{V}$$
8		eqid	$$⊢\left(n\in N⟼\left\{U,n\right\}\right)=\left(n\in N⟼\left\{U,n\right\}\right)$$
9	1 2 3 4 8	nbusgrf1o0	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \left(n\in N⟼\left\{U,n\right\}\right):N\underset{1-1\; onto}{⟶}I$$
10		f1oeq1	$$⊢f=\left(n\in N⟼\left\{U,n\right\}\right)\to \left(f:N\underset{1-1\; onto}{⟶}I\leftrightarrow \left(n\in N⟼\left\{U,n\right\}\right):N\underset{1-1\; onto}{⟶}I\right)$$
11	7 9 10	spcedv	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \exists ff:N\underset{1-1\; onto}{⟶}I$$