Theorem edgusgrnbfin

Description: The number of neighbors of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 28-Oct-2020)

	Ref	Expression
Hypotheses	nbusgrf1o.v	|- V = ( Vtx ` G )
	nbusgrf1o.e	|- E = ( Edg ` G )
Assertion	edgusgrnbfin	|- ( ( G e. USGraph /\ U e. V ) -> ( ( G NeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o.v	|- V = ( Vtx ` G )
2		nbusgrf1o.e	|- E = ( Edg ` G )
3	1 2	nbusgrf1o	|- ( ( G e. USGraph /\ U e. V ) -> E. f f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } )
4		f1ofo	|- ( f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } -> f : ( G NeighbVtx U ) -onto-> { e e. E | U e. e } )
5		fofi	|- ( ( ( G NeighbVtx U ) e. Fin /\ f : ( G NeighbVtx U ) -onto-> { e e. E | U e. e } ) -> { e e. E | U e. e } e. Fin )
6	5	expcom	|- ( f : ( G NeighbVtx U ) -onto-> { e e. E | U e. e } -> ( ( G NeighbVtx U ) e. Fin -> { e e. E | U e. e } e. Fin ) )
7	4 6	syl	|- ( f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } -> ( ( G NeighbVtx U ) e. Fin -> { e e. E | U e. e } e. Fin ) )
8	7	exlimiv	|- ( E. f f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } -> ( ( G NeighbVtx U ) e. Fin -> { e e. E | U e. e } e. Fin ) )
9	3 8	syl	|- ( ( G e. USGraph /\ U e. V ) -> ( ( G NeighbVtx U ) e. Fin -> { e e. E | U e. e } e. Fin ) )
10		f1of1	|- ( f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } -> f : ( G NeighbVtx U ) -1-1-> { e e. E | U e. e } )
11		f1fi	|- ( ( { e e. E | U e. e } e. Fin /\ f : ( G NeighbVtx U ) -1-1-> { e e. E | U e. e } ) -> ( G NeighbVtx U ) e. Fin )
12	11	expcom	|- ( f : ( G NeighbVtx U ) -1-1-> { e e. E | U e. e } -> ( { e e. E | U e. e } e. Fin -> ( G NeighbVtx U ) e. Fin ) )
13	10 12	syl	|- ( f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } -> ( { e e. E | U e. e } e. Fin -> ( G NeighbVtx U ) e. Fin ) )
14	13	exlimiv	|- ( E. f f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } -> ( { e e. E | U e. e } e. Fin -> ( G NeighbVtx U ) e. Fin ) )
15	3 14	syl	|- ( ( G e. USGraph /\ U e. V ) -> ( { e e. E | U e. e } e. Fin -> ( G NeighbVtx U ) e. Fin ) )
16	9 15	impbid	|- ( ( G e. USGraph /\ U e. V ) -> ( ( G NeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) )