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 
|- ( ( 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 0fi 
 |-  (/) 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 )