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

Metamath Proof Explorer

Theorem upgrfn

Description: The edge function of an undirected pseudograph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

		Ref	Expression
	Hypotheses	isupgr.v	$⊢ V = Vtx (G)$
		isupgr.e	$⊢ E = iEdg (G)$
	Assertion	upgrfn	$⊢ (G \in UPGraph \land E Fn A) \to E : A ⟶ \{x \in (𝒫 V ∖ \{\emptyset\}) \| \|x\| \leq 2\}$

Proof

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