Theorem uspgrspren

Description: The set G of the "simple pseudographs" with a fixed set of vertices V and the class P of subsets of the set of pairs over the fixed set V are equinumerous. (Contributed by AV, 27-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\}$$
Assertion	uspgrspren	$$⊢V\in W\to G\approx 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	1 2	uspgrbispr	$$⊢V\in W\to \exists ff:G\underset{1-1\; onto}{⟶}P$$
4		bren	$$⊢G\approx P\leftrightarrow \exists ff:G\underset{1-1\; onto}{⟶}P$$
5	3 4	sylibr	$$⊢V\in W\to G\approx P$$