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

Metamath Proof Explorer

Theorem uhgr0vsize0

Description: The size of a hypergraph with no vertices (the null graph) is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018) (Revised by AV, 7-Nov-2020)

Ref Expression
Hypotheses uhgr0v0e.v 
|- V = ( Vtx ` G )
uhgr0v0e.e 
|- E = ( Edg ` G )
Assertion uhgr0vsize0 
|- ( ( G e. UHGraph /\ ( # ` V ) = 0 ) -> ( # ` E ) = 0 )

Proof

Step Hyp Ref Expression
1 uhgr0v0e.v 
 |-  V = ( Vtx ` G )
2 uhgr0v0e.e 
 |-  E = ( Edg ` G )
3 1 2 uhgr0v0e 
 |-  ( ( G e. UHGraph /\ V = (/) ) -> E = (/) )
4 3 ex 
 |-  ( G e. UHGraph -> ( V = (/) -> E = (/) ) )
5 1 fvexi 
 |-  V e. _V
6 hasheq0 
 |-  ( V e. _V -> ( ( # ` V ) = 0 <-> V = (/) ) )
7 5 6 ax-mp 
 |-  ( ( # ` V ) = 0 <-> V = (/) )
8 2 fvexi 
 |-  E e. _V
9 hasheq0 
 |-  ( E e. _V -> ( ( # ` E ) = 0 <-> E = (/) ) )
10 8 9 ax-mp 
 |-  ( ( # ` E ) = 0 <-> E = (/) )
11 4 7 10 3imtr4g 
 |-  ( G e. UHGraph -> ( ( # ` V ) = 0 -> ( # ` E ) = 0 ) )
12 11 imp 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 0 ) -> ( # ` E ) = 0 )