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 0fin ⊢∅∈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