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