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 )