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 )