uhgr0vusgr

Description: The null graph, with no vertices, represented by a hypergraph, is a simple graph. (Contributed by AV, 5-Dec-2020)

		Ref	Expression
	Assertion	uhgr0vusgr	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to G \in USGraph$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to G \in UHGraph$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3		eqid	$⊢ Edg (G) = Edg (G)$
4	2 3	uhgr0v0e	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to Edg (G) = \emptyset$
5		uhgriedg0edg0	$⊢ G \in UHGraph \to (Edg (G) = \emptyset \leftrightarrow iEdg (G) = \emptyset)$
6	5	adantr	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to (Edg (G) = \emptyset \leftrightarrow iEdg (G) = \emptyset)$
7	4 6	mpbid	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to iEdg (G) = \emptyset$
8	1 7	usgr0e	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to G \in USGraph$

Metamath Proof Explorer