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

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→ 𝐼 )