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 )