Theorem uspgrex

Description: The class G of all "simple pseudographs" with a fixed set of vertices V is a set. (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	uspgrex	$$⊢V\in W\to G\in \mathrm{V}$$

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		fvex	$$⊢\mathrm{Pairs}\left(V\right)\in \mathrm{V}$$
4	3	pwex	$$⊢𝒫\mathrm{Pairs}\left(V\right)\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢P\in \mathrm{V}$$
6		eqid	$$⊢\left(g\in G⟼2^{nd}\left(g\right)\right)=\left(g\in G⟼2^{nd}\left(g\right)\right)$$
7	1 2 6	uspgrsprf1o	$$⊢V\in W\to \left(g\in G⟼2^{nd}\left(g\right)\right):G\underset{1-1\; onto}{⟶}P$$
8		f1ovv	$$⊢\left(g\in G⟼2^{nd}\left(g\right)\right):G\underset{1-1\; onto}{⟶}P\to \left(G\in \mathrm{V}\leftrightarrow P\in \mathrm{V}\right)$$
9	7 8	syl	$$⊢V\in W\to \left(G\in \mathrm{V}\leftrightarrow P\in \mathrm{V}\right)$$
10	5 9	mpbiri	$$⊢V\in W\to G\in \mathrm{V}$$