Theorem uspgrsprf1o

Description: The mapping F is a bijection between the "simple pseudographs" with a fixed set of vertices V and the subsets of the set of pairs over the set V . See also the comments on uspgrbisymrel . (Contributed by AV, 25-Nov-2021)

	Ref	Expression
Hypotheses	uspgrsprf.p	$$⊢P=𝒫\mathrm{Pairs}\left(V\right)$$
	uspgrsprf.g	$$⊢G=\left\{⟨v,e⟩|\left(v=V\wedge \exists q\in \mathrm{USHGraph}\left(\mathrm{Vtx}\left(q\right)=v\wedge \mathrm{Edg}\left(q\right)=e\right)\right)\right\}$$
	uspgrsprf.f	$$⊢F=\left(g\in G⟼2^{nd}\left(g\right)\right)$$
Assertion	uspgrsprf1o	$$⊢V\in W\to F:G\underset{1-1\; onto}{⟶}P$$

Proof

Step	Hyp	Ref	Expression
1		uspgrsprf.p	$$⊢P=𝒫\mathrm{Pairs}\left(V\right)$$
2		uspgrsprf.g	$$⊢G=\left\{⟨v,e⟩|\left(v=V\wedge \exists q\in \mathrm{USHGraph}\left(\mathrm{Vtx}\left(q\right)=v\wedge \mathrm{Edg}\left(q\right)=e\right)\right)\right\}$$
3		uspgrsprf.f	$$⊢F=\left(g\in G⟼2^{nd}\left(g\right)\right)$$
4	1 2 3	uspgrsprf1	$$⊢F:G\underset{1-1}{⟶}P$$
5	4	a1i	$$⊢V\in W\to F:G\underset{1-1}{⟶}P$$
6	1 2 3	uspgrsprfo	$$⊢V\in W\to F:G\underset{onto}{⟶}P$$
7		df-f1o	$$⊢F:G\underset{1-1\; onto}{⟶}P\leftrightarrow \left(F:G\underset{1-1}{⟶}P\wedge F:G\underset{onto}{⟶}P\right)$$
8	5 6 7	sylanbrc	$$⊢V\in W\to F:G\underset{1-1\; onto}{⟶}P$$