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 \in UHGraph \land \|V\| = 0) \to \|E\| = 0$

Proof

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