Theorem uspgrymrelen

Description: The set G of the "simple pseudographs" with a fixed set of vertices V and the class R of the symmetric relations on the fixed set V are equinumerous. For more details about the class G of all "simple pseudographs" see comments on uspgrbisymrel . (Contributed by AV, 27-Nov-2021)

	Ref	Expression
Hypotheses	uspgrbisymrel.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\}$$
	uspgrbisymrel.r	$$⊢R=\left\{r\in 𝒫\left(V\times V\right)|\forall x\in V\forall y\in V\left(xry\leftrightarrow yrx\right)\right\}$$
Assertion	uspgrymrelen	$$⊢V\in W\to G\approx R$$

Proof

Step	Hyp	Ref	Expression
1		uspgrbisymrel.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\}$$
2		uspgrbisymrel.r	$$⊢R=\left\{r\in 𝒫\left(V\times V\right)|\forall x\in V\forall y\in V\left(xry\leftrightarrow yrx\right)\right\}$$
3		eqid	$$⊢𝒫\mathrm{Pairs}\left(V\right)=𝒫\mathrm{Pairs}\left(V\right)$$
4	3 1	uspgrspren	$$⊢V\in W\to G\approx 𝒫\mathrm{Pairs}\left(V\right)$$
5	3 2	sprsymrelen	$$⊢V\in W\to 𝒫\mathrm{Pairs}\left(V\right)\approx R$$
6		entr	$$⊢\left(G\approx 𝒫\mathrm{Pairs}\left(V\right)\wedge 𝒫\mathrm{Pairs}\left(V\right)\approx R\right)\to G\approx R$$
7	4 5 6	syl2anc	$$⊢V\in W\to G\approx R$$