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

Metamath Proof Explorer

Theorem usgredgffibi

Description: The number of edges in a simple graph is finite iff its edge function is finite. (Contributed by AV, 10-Jan-2020) (Revised by AV, 22-Oct-2020)

Ref Expression
Hypotheses usgredgffibi.I 
|- I = ( iEdg ` G )
usgredgffibi.e 
|- E = ( Edg ` G )
Assertion usgredgffibi 
|- ( G e. USGraph -> ( E e. Fin <-> I e. Fin ) )

Proof

Step Hyp Ref Expression
1 usgredgffibi.I 
 |-  I = ( iEdg ` G )
2 usgredgffibi.e 
 |-  E = ( Edg ` G )
3 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
4 1 eqcomi 
 |-  ( iEdg ` G ) = I
5 4 rneqi 
 |-  ran ( iEdg ` G ) = ran I
6 2 3 5 3eqtri 
 |-  E = ran I
7 6 eleq1i 
 |-  ( E e. Fin <-> ran I e. Fin )
8 1 fvexi 
 |-  I e. _V
9 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
10 9 1 usgrfs 
 |-  ( G e. USGraph -> I : dom I -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
11 f1vrnfibi 
 |-  ( ( I e. _V /\ I : dom I -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) -> ( I e. Fin <-> ran I e. Fin ) )
12 8 10 11 sylancr 
 |-  ( G e. USGraph -> ( I e. Fin <-> ran I e. Fin ) )
13 7 12 bitr4id 
 |-  ( G e. USGraph -> ( E e. Fin <-> I e. Fin ) )