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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	nbusgrf1o1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	nbusgrf1o1.n	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑈 )
	nbusgrf1o1.i	⊢ 𝐼 = { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 }
Assertion	nbusgrf1o1	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : 𝑁 –1-1-onto→ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		nbusgrf1o1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		nbusgrf1o1.n	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑈 )
4		nbusgrf1o1.i	⊢ 𝐼 = { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 }
5	3	ovexi	⊢ 𝑁 ∈ V
6		mptexg	⊢ ( 𝑁 ∈ V → ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } ) ∈ V )
7	5 6	mp1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } ) ∈ V )
8		eqid	⊢ ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } ) = ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } )
9	1 2 3 4 8	nbusgrf1o0	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } ) : 𝑁 –1-1-onto→ 𝐼 )
10		f1oeq1	⊢ ( 𝑓 = ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝐼 ↔ ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } ) : 𝑁 –1-1-onto→ 𝐼 ) )
11	7 9 10	spcedv	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : 𝑁 –1-1-onto→ 𝐼 )