# Metamath Proof Explorer

## Theorem upgrf

Description: The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfn without explicitly specified domain of the edge function. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Hypotheses isupgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
isupgr.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
Assertion upgrf ${⊢}{G}\in \mathrm{UPGraph}\to {E}:\mathrm{dom}{E}⟶\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$

### Proof

Step Hyp Ref Expression
1 isupgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 isupgr.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 1 2 isupgr ${⊢}{G}\in \mathrm{UPGraph}\to \left({G}\in \mathrm{UPGraph}↔{E}:\mathrm{dom}{E}⟶\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}\right)$
4 3 ibi ${⊢}{G}\in \mathrm{UPGraph}\to {E}:\mathrm{dom}{E}⟶\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$