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 = ~P ( Pairs ` V )
	uspgrsprf.g	|- G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
	uspgrsprf.f	|- F = ( g e. G |-> ( 2nd ` g ) )
Assertion	uspgrsprfv	|- ( X e. G -> ( F ` X ) = ( 2nd ` X ) )

Proof

Step	Hyp	Ref	Expression
1		uspgrsprf.p	|- P = ~P ( Pairs ` V )
2		uspgrsprf.g	|- G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
3		uspgrsprf.f	|- F = ( g e. G |-> ( 2nd ` g ) )
4		fveq2	|- ( g = X -> ( 2nd ` g ) = ( 2nd ` X ) )
5		id	|- ( X e. G -> X e. G )
6		fvexd	|- ( X e. G -> ( 2nd ` X ) e. _V )
7	3 4 5 6	fvmptd3	|- ( X e. G -> ( F ` X ) = ( 2nd ` X ) )