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 ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 0 ) → ( Edg ‘ 𝐺 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 uhgr0vsize0 ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 0 ) → ( ♯ ‘ ( Edg ‘ 𝐺 ) ) = 0 )
4 fvex ( Edg ‘ 𝐺 ) ∈ V
5 hasheq0 ( ( Edg ‘ 𝐺 ) ∈ V → ( ( ♯ ‘ ( Edg ‘ 𝐺 ) ) = 0 ↔ ( Edg ‘ 𝐺 ) = ∅ ) )
6 4 5 ax-mp ( ( ♯ ‘ ( Edg ‘ 𝐺 ) ) = 0 ↔ ( Edg ‘ 𝐺 ) = ∅ )
7 0fin ∅ ∈ Fin
8 eleq1 ( ( Edg ‘ 𝐺 ) = ∅ → ( ( Edg ‘ 𝐺 ) ∈ Fin ↔ ∅ ∈ Fin ) )
9 7 8 mpbiri ( ( Edg ‘ 𝐺 ) = ∅ → ( Edg ‘ 𝐺 ) ∈ Fin )
10 6 9 sylbi ( ( ♯ ‘ ( Edg ‘ 𝐺 ) ) = 0 → ( Edg ‘ 𝐺 ) ∈ Fin )
11 3 10 syl ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 0 ) → ( Edg ‘ 𝐺 ) ∈ Fin )