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 e. UHGraph /\ ( # ` ( Vtx ` G ) ) = 0 ) -> ( Edg ` G ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
2		eqid	|- ( Edg ` G ) = ( Edg ` G )
3	1 2	uhgr0vsize0	|- ( ( G e. UHGraph /\ ( # ` ( Vtx ` G ) ) = 0 ) -> ( # ` ( Edg ` G ) ) = 0 )
4		fvex	|- ( Edg ` G ) e. _V
5		hasheq0	|- ( ( Edg ` G ) e. _V -> ( ( # ` ( Edg ` G ) ) = 0 <-> ( Edg ` G ) = (/) ) )
6	4 5	ax-mp	|- ( ( # ` ( Edg ` G ) ) = 0 <-> ( Edg ` G ) = (/) )
7		0fin	|- (/) e. Fin
8		eleq1	|- ( ( Edg ` G ) = (/) -> ( ( Edg ` G ) e. Fin <-> (/) e. Fin ) )
9	7 8	mpbiri	|- ( ( Edg ` G ) = (/) -> ( Edg ` G ) e. Fin )
10	6 9	sylbi	|- ( ( # ` ( Edg ` G ) ) = 0 -> ( Edg ` G ) e. Fin )
11	3 10	syl	|- ( ( G e. UHGraph /\ ( # ` ( Vtx ` G ) ) = 0 ) -> ( Edg ` G ) e. Fin )