Metamath Proof Explorer

Theorem umgr0e

Description: The empty graph, with vertices but no edges, is a multigraph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 25-Nov-2020)

		Ref	Expression
	Hypotheses	umgr0e.g	$⊢ φ \to G \in W$
		umgr0e.e	$⊢ φ \to iEdg (G) = \emptyset$
	Assertion	umgr0e	$⊢ φ \to G \in UMGraph$

Proof

Step	Hyp	Ref	Expression
1		umgr0e.g	$⊢ φ \to G \in W$
2		umgr0e.e	$⊢ φ \to iEdg (G) = \emptyset$
3	2	f10d	$⊢ φ \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| = 2\}$
4		f1f	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| = 2\} \to iEdg (G) : dom iEdg (G) ⟶ \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| = 2\}$
5	3 4	syl	$⊢ φ \to iEdg (G) : dom iEdg (G) ⟶ \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| = 2\}$
6		eqid	$⊢ Vtx (G) = Vtx (G)$
7		eqid	$⊢ iEdg (G) = iEdg (G)$
8	6 7	isumgr	$⊢ G \in W \to (G \in UMGraph \leftrightarrow iEdg (G) : dom iEdg (G) ⟶ \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| = 2\})$
9	1 8	syl	$⊢ φ \to (G \in UMGraph \leftrightarrow iEdg (G) : dom iEdg (G) ⟶ \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| = 2\})$
10	5 9	mpbird	$⊢ φ \to G \in UMGraph$