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|N∉e
Assertion usgrfilem ⊢G∈FinUSGraph∧N∈V→E∈Fin↔F∈Fin

Proof

Step Hyp Ref Expression
1 fusgredgfi.v ⊢V=Vtx⁡G
2 fusgredgfi.e ⊢E=Edg⁡G
3 usgrfilem.f ⊢F=e∈E|N∉e
4 rabfi ⊢E∈Fin→e∈E|N∉e∈Fin
5 3 4 eqeltrid ⊢E∈Fin→F∈Fin
6 uncom ⊢F∪e∈E|N∈e=e∈E|N∈e∪F
7 eqid ⊢e∈E|N∈e=e∈E|N∈e
8 7 3 elnelun ⊢e∈E|N∈e∪F=E
9 6 8 eqtr2i ⊢E=F∪e∈E|N∈e
10 1 2 fusgredgfi ⊢G∈FinUSGraph∧N∈V→e∈E|N∈e∈Fin
11 10 anim1ci ⊢G∈FinUSGraph∧N∈V∧F∈Fin→F∈Fin∧e∈E|N∈e∈Fin
12 unfi ⊢F∈Fin∧e∈E|N∈e∈Fin→F∪e∈E|N∈e∈Fin
13 11 12 syl ⊢G∈FinUSGraph∧N∈V∧F∈Fin→F∪e∈E|N∈e∈Fin
14 9 13 eqeltrid ⊢G∈FinUSGraph∧N∈V∧F∈Fin→E∈Fin
15 14 ex ⊢G∈FinUSGraph∧N∈V→F∈Fin→E∈Fin
16 5 15 impbid2 ⊢G∈FinUSGraph∧N∈V→E∈Fin↔F∈Fin