Metamath Proof Explorer

Theorem uhgr0edgfi

Description: A graph of order 0 (i.e. with 0 vertices) has a finite set of edges. (Contributed by Alexander van der Vekens, 5-Jan-2018) (Revised by AV, 10-Jan-2020) (Revised by AV, 8-Jun-2021)

Ref Expression
Assertion uhgr0edgfi ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = 0 → Edg ⁡ G ∈ Fin

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 uhgr0vsize0 ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = 0 → Edg ⁡ G = 0
4 fvex ⊢ Edg ⁡ G ∈ V
5 hasheq0 ⊢ Edg ⁡ G ∈ V → Edg ⁡ G = 0 ↔ Edg ⁡ G = ∅
6 4 5 ax-mp ⊢ Edg ⁡ G = 0 ↔ Edg ⁡ G = ∅
7 0fi ⊢ ∅ ∈ Fin
8 eleq1 ⊢ Edg ⁡ G = ∅ → Edg ⁡ G ∈ Fin ↔ ∅ ∈ Fin
9 7 8 mpbiri ⊢ Edg ⁡ G = ∅ → Edg ⁡ G ∈ Fin
10 6 9 sylbi ⊢ Edg ⁡ G = 0 → Edg ⁡ G ∈ Fin
11 3 10 syl ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = 0 → Edg ⁡ G ∈ Fin