Metamath Proof Explorer

Theorem usgr0eop

Description: The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020)

		Ref	Expression
	Assertion	usgr0eop	$⊢ V \in W \to ⟨V, \emptyset⟩ \in USGraph$

Proof

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨V, \emptyset⟩ \in V$
2	1	a1i	$⊢ V \in W \to ⟨V, \emptyset⟩ \in V$
3		0ex	$⊢ \emptyset \in V$
4		opiedgfv	$⊢ (V \in W \land \emptyset \in V) \to iEdg (⟨V, \emptyset⟩) = \emptyset$
5	3 4	mpan2	$⊢ V \in W \to iEdg (⟨V, \emptyset⟩) = \emptyset$
6	2 5	usgr0e	$⊢ V \in W \to ⟨V, \emptyset⟩ \in USGraph$