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 = ~P ( Pairs ` V )
	uspgrsprf.g	|- G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
Assertion	uspgrex	|- ( V e. W -> G e. _V )

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		fvex	|- ( Pairs ` V ) e. _V
4	3	pwex	|- ~P ( Pairs ` V ) e. _V
5	1 4	eqeltri	|- P e. _V
6		eqid	|- ( g e. G |-> ( 2nd ` g ) ) = ( g e. G |-> ( 2nd ` g ) )
7	1 2 6	uspgrsprf1o	|- ( V e. W -> ( g e. G |-> ( 2nd ` g ) ) : G -1-1-onto-> P )
8		f1ovv	|- ( ( g e. G |-> ( 2nd ` g ) ) : G -1-1-onto-> P -> ( G e. _V <-> P e. _V ) )
9	7 8	syl	|- ( V e. W -> ( G e. _V <-> P e. _V ) )
10	5 9	mpbiri	|- ( V e. W -> G e. _V )