This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem umgrf

Description: The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfn without explicitly specified domain of the edge function. (Contributed by AV, 24-Nov-2020)

	Ref	Expression
Hypotheses	isumgr.v	$⊢ V = Vtx (G)$
	isumgr.e	$⊢ E = iEdg (G)$
Assertion	umgrf	$⊢ G \in UMGraph \to E : dom E ⟶ \{x \in 𝒫 V \| \|x\| = 2\}$

Proof

Step	Hyp	Ref	Expression
1		isumgr.v	$⊢ V = Vtx (G)$
2		isumgr.e	$⊢ E = iEdg (G)$
3	1 2	isumgrs	$⊢ G \in UMGraph \to (G \in UMGraph \leftrightarrow E : dom E ⟶ \{x \in 𝒫 V \| \|x\| = 2\})$
4	3	ibi	$⊢ G \in UMGraph \to E : dom E ⟶ \{x \in 𝒫 V \| \|x\| = 2\}$