Theorem usgrfilem

Description: In a finite simple graph, the number of edges is finite iff the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 9-Nov-2020)

	Ref	Expression
Hypotheses	fusgredgfi.v	|- V = ( Vtx ` G )
	fusgredgfi.e	|- E = ( Edg ` G )
	usgrfilem.f	|- F = { e e. E | N e/ e }
Assertion	usgrfilem	|- ( ( G e. FinUSGraph /\ N e. V ) -> ( E e. Fin <-> F e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		fusgredgfi.v	|- V = ( Vtx ` G )
2		fusgredgfi.e	|- E = ( Edg ` G )
3		usgrfilem.f	|- F = { e e. E | N e/ e }
4		rabfi	|- ( E e. Fin -> { e e. E | N e/ e } e. Fin )
5	3 4	eqeltrid	|- ( E e. Fin -> F e. Fin )
6		uncom	|- ( F u. { e e. E | N e. e } ) = ( { e e. E | N e. e } u. F )
7		eqid	|- { e e. E | N e. e } = { e e. E | N e. e }
8	7 3	elnelun	|- ( { e e. E | N e. e } u. F ) = E
9	6 8	eqtr2i	|- E = ( F u. { e e. E | N e. e } )
10	1 2	fusgredgfi	|- ( ( G e. FinUSGraph /\ N e. V ) -> { e e. E | N e. e } e. Fin )
11	10	anim1ci	|- ( ( ( G e. FinUSGraph /\ N e. V ) /\ F e. Fin ) -> ( F e. Fin /\ { e e. E | N e. e } e. Fin ) )
12		unfi	|- ( ( F e. Fin /\ { e e. E | N e. e } e. Fin ) -> ( F u. { e e. E | N e. e } ) e. Fin )
13	11 12	syl	|- ( ( ( G e. FinUSGraph /\ N e. V ) /\ F e. Fin ) -> ( F u. { e e. E | N e. e } ) e. Fin )
14	9 13	eqeltrid	|- ( ( ( G e. FinUSGraph /\ N e. V ) /\ F e. Fin ) -> E e. Fin )
15	14	ex	|- ( ( G e. FinUSGraph /\ N e. V ) -> ( F e. Fin -> E e. Fin ) )
16	5 15	impbid2	|- ( ( G e. FinUSGraph /\ N e. V ) -> ( E e. Fin <-> F e. Fin ) )