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=\mathrm{Vtx}\left(G\right)$$
	uhgr0v0e.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	uhgr0vsize0	$$⊢\left(G\in \mathrm{UHGraph}\wedge \left|V\right|=0\right)\to \left|E\right|=0$$

Proof

Step	Hyp	Ref	Expression
1		uhgr0v0e.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		uhgr0v0e.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3	1 2	uhgr0v0e	$$⊢\left(G\in \mathrm{UHGraph}\wedge V=\varnothing \right)\to E=\varnothing$$
4	3	ex	$$⊢G\in \mathrm{UHGraph}\to \left(V=\varnothing \to E=\varnothing \right)$$
5	1	fvexi	$$⊢V\in \mathrm{V}$$
6		hasheq0	$$⊢V\in \mathrm{V}\to \left(\left|V\right|=0\leftrightarrow V=\varnothing \right)$$
7	5 6	ax-mp	$$⊢\left|V\right|=0\leftrightarrow V=\varnothing$$
8	2	fvexi	$$⊢E\in \mathrm{V}$$
9		hasheq0	$$⊢E\in \mathrm{V}\to \left(\left|E\right|=0\leftrightarrow E=\varnothing \right)$$
10	8 9	ax-mp	$$⊢\left|E\right|=0\leftrightarrow E=\varnothing$$
11	4 7 10	3imtr4g	$$⊢G\in \mathrm{UHGraph}\to \left(\left|V\right|=0\to \left|E\right|=0\right)$$
12	11	imp	$$⊢\left(G\in \mathrm{UHGraph}\wedge \left|V\right|=0\right)\to \left|E\right|=0$$