This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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