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 ⊢ V = Vtx ⁡ G
nbusgrf1o.e ⊢ E = Edg ⁡ G
Assertion nbusgrf1o ⊢ G ∈ USGraph ∧ U ∈ V → ∃ f f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e

Proof

Step Hyp Ref Expression
1 nbusgrf1o.v ⊢ V = Vtx ⁡ G
2 nbusgrf1o.e ⊢ E = Edg ⁡ G
3 eqid ⊢ G NeighbVtx U = G NeighbVtx U
4 eleq2w ⊢ e = c → U ∈ e ↔ U ∈ c
5 4 cbvrabv ⊢ e ∈ E | U ∈ e = c ∈ E | U ∈ c
6 1 2 3 5 nbusgrf1o1 ⊢ G ∈ USGraph ∧ U ∈ V → ∃ f f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e