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