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 
|- V = ( Vtx ` G )
nbusgrf1o1.e 
|- E = ( Edg ` G )
nbusgrf1o1.n 
|- N = ( G NeighbVtx U )
nbusgrf1o1.i 
|- I = { e e. E | U e. e }
Assertion nbusgrf1o1 
|- ( ( G e. USGraph /\ U e. V ) -> E. 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. E | U e. e }
5 3 ovexi 
 |-  N e. _V
6 mptexg 
 |-  ( N e. _V -> ( n e. N |-> { U , n } ) e. _V )
7 5 6 mp1i 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( n e. N |-> { U , n } ) e. _V )
8 eqid 
 |-  ( n e. N |-> { U , n } ) = ( n e. N |-> { U , n } )
9 1 2 3 4 8 nbusgrf1o0 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( n e. N |-> { U , n } ) : N -1-1-onto-> I )
10 f1oeq1 
 |-  ( f = ( n e. N |-> { U , n } ) -> ( f : N -1-1-onto-> I <-> ( n e. N |-> { U , n } ) : N -1-1-onto-> I ) )
11 7 9 10 spcedv 
 |-  ( ( G e. USGraph /\ U e. V ) -> E. f f : N -1-1-onto-> I )