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

Metamath Proof Explorer

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