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=VtxG
fusgredgfi.e E=EdgG
usgrfilem.f F=eE|Ne
Assertion usgrfilem GFinUSGraphNVEFinFFin

Proof

Step Hyp Ref Expression
1 fusgredgfi.v V=VtxG
2 fusgredgfi.e E=EdgG
3 usgrfilem.f F=eE|Ne
4 rabfi EFineE|NeFin
5 3 4 eqeltrid EFinFFin
6 uncom FeE|Ne=eE|NeF
7 eqid eE|Ne=eE|Ne
8 7 3 elnelun eE|NeF=E
9 6 8 eqtr2i E=FeE|Ne
10 1 2 fusgredgfi GFinUSGraphNVeE|NeFin
11 10 anim1ci GFinUSGraphNVFFinFFineE|NeFin
12 unfi FFineE|NeFinFeE|NeFin
13 11 12 syl GFinUSGraphNVFFinFeE|NeFin
14 9 13 eqeltrid GFinUSGraphNVFFinEFin
15 14 ex GFinUSGraphNVFFinEFin
16 5 15 impbid2 GFinUSGraphNVEFinFFin