Theorem uspgrf1oedg

Description: The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020) (Revised by AV, 15-Oct-2020)

	Ref	Expression
Hypothesis	usgrf1o.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
Assertion	uspgrf1oedg	$$⊢G\in \mathrm{USHGraph}\to E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\mathrm{Edg}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		usgrf1o.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
2		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
3	2 1	uspgrf	$$⊢G\in \mathrm{USHGraph}\to E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in \left(𝒫\mathrm{Vtx}\left(G\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
4		f1f1orn	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in \left(𝒫\mathrm{Vtx}\left(G\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\to E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\mathrm{ran}E$$
5	1	rneqi	$$⊢\mathrm{ran}E=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
6		edgval	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
7	5 6	eqtr4i	$$⊢\mathrm{ran}E=\mathrm{Edg}\left(G\right)$$
8		f1oeq3	$$⊢\mathrm{ran}E=\mathrm{Edg}\left(G\right)\to \left(E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\mathrm{ran}E\leftrightarrow E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\mathrm{Edg}\left(G\right)\right)$$
9	7 8	ax-mp	$$⊢E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\mathrm{ran}E\leftrightarrow E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\mathrm{Edg}\left(G\right)$$
10	4 9	sylib	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in \left(𝒫\mathrm{Vtx}\left(G\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\to E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\mathrm{Edg}\left(G\right)$$
11	3 10	syl	$$⊢G\in \mathrm{USHGraph}\to E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\mathrm{Edg}\left(G\right)$$