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

Metamath Proof Explorer

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