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

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		nbusgrf1o.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		eqid	⊢ ( 𝐺 NeighbVtx 𝑈 ) = ( 𝐺 NeighbVtx 𝑈 )
4		eleq2w	⊢ ( 𝑒 = 𝑐 → ( 𝑈 ∈ 𝑒 ↔ 𝑈 ∈ 𝑐 ) )
5	4	cbvrabv	⊢ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } = { 𝑐 ∈ 𝐸 ∣ 𝑈 ∈ 𝑐 }
6	1 2 3 5	nbusgrf1o1	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )