Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 nbusgrf1o1.v ⊢ V = Vtx ⁡ G
2 nbusgrf1o1.e ⊢ E = Edg ⁡ G
3 nbusgrf1o1.n ⊢ N = G NeighbVtx U
4 nbusgrf1o1.i ⊢ I = e ∈ E | U ∈ e
5 3 ovexi ⊢ N ∈ V
6 mptexg ⊢ N ∈ V → n ∈ N ⟼ U n ∈ V
7 5 6 mp1i ⊢ G ∈ USGraph ∧ U ∈ V → n ∈ N ⟼ U n ∈ V
8 eqid ⊢ n ∈ N ⟼ U n = n ∈ N ⟼ U n
9 1 2 3 4 8 nbusgrf1o0 ⊢ G ∈ USGraph ∧ U ∈ V → n ∈ N ⟼ U n : N ⟶ 1-1 onto I
10 f1oeq1 ⊢ f = n ∈ N ⟼ U n → f : N ⟶ 1-1 onto I ↔ n ∈ N ⟼ U n : N ⟶ 1-1 onto I
11 7 9 10 spcedv ⊢ G ∈ USGraph ∧ U ∈ V → ∃ f f : N ⟶ 1-1 onto I