Theorem uspgrbispr

Description: There 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 . (Contributed by AV, 26-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	uspgrbispr	$$⊢V\in W\to \exists ff: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	1 2	uspgrex	$$⊢V\in W\to G\in \mathrm{V}$$
4	3	mptexd	$$⊢V\in W\to \left(g\in G⟼2^{nd}\left(g\right)\right)\in \mathrm{V}$$
5		eqid	$$⊢\left(g\in G⟼2^{nd}\left(g\right)\right)=\left(g\in G⟼2^{nd}\left(g\right)\right)$$
6	1 2 5	uspgrsprf1o	$$⊢V\in W\to \left(g\in G⟼2^{nd}\left(g\right)\right):G\underset{1-1\; onto}{⟶}P$$
7		f1oeq1	$$⊢f=\left(g\in G⟼2^{nd}\left(g\right)\right)\to \left(f:G\underset{1-1\; onto}{⟶}P\leftrightarrow \left(g\in G⟼2^{nd}\left(g\right)\right):G\underset{1-1\; onto}{⟶}P\right)$$
8	4 6 7	spcedv	$$⊢V\in W\to \exists ff:G\underset{1-1\; onto}{⟶}P$$