umgrfn

Description: The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by AV, 24-Nov-2020)

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

Step	Hyp	Ref	Expression
1		isumgr.v	$⊢ V = Vtx (G)$
2		isumgr.e	$⊢ E = iEdg (G)$
3	1 2	umgrf	$⊢ G \in UMGraph \to E : dom E ⟶ \{x \in 𝒫 V \| \|x\| = 2\}$
4		fndm	$⊢ E Fn A \to dom E = A$
5	4	feq2d	$⊢ E Fn A \to (E : dom E ⟶ \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow E : A ⟶ \{x \in 𝒫 V \| \|x\| = 2\})$
6	3 5	syl5ibcom	$⊢ G \in UMGraph \to (E Fn A \to E : A ⟶ \{x \in 𝒫 V \| \|x\| = 2\})$
7	6	imp	$⊢ (G \in UMGraph \land E Fn A) \to E : A ⟶ \{x \in 𝒫 V \| \|x\| = 2\}$

Metamath Proof Explorer