This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )