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 𝑉 = ( 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𝐼 )