Theorem uspgrsprfv

Description: The value of the function F which maps a "simple pseudograph" for a fixed set V of vertices to the set of edges (i.e. range of the edge function) of the graph. Solely for G as defined here, the function F is a bijection between the "simple pseudographs" and the subsets of the set of pairs P over the fixed set V of vertices, see uspgrbispr . (Contributed by AV, 24-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	uspgrsprfv	$$⊢X\in G\to F\left(X\right)=2^{nd}\left(X\right)$$

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		fveq2	$$⊢g=X\to 2^{nd}\left(g\right)=2^{nd}\left(X\right)$$
5		id	$$⊢X\in G\to X\in G$$
6		fvexd	$$⊢X\in G\to 2^{nd}\left(X\right)\in \mathrm{V}$$
7	3 4 5 6	fvmptd3	$$⊢X\in G\to F\left(X\right)=2^{nd}\left(X\right)$$