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

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	1 2	uspgrex	|- ( V e. W -> G e. _V )
4	3	mptexd	|- ( V e. W -> ( g e. G |-> ( 2nd ` g ) ) e. _V )
5		eqid	|- ( g e. G |-> ( 2nd ` g ) ) = ( g e. G |-> ( 2nd ` g ) )
6	1 2 5	uspgrsprf1o	|- ( V e. W -> ( g e. G |-> ( 2nd ` g ) ) : G -1-1-onto-> P )
7		f1oeq1	|- ( f = ( g e. G |-> ( 2nd ` g ) ) -> ( f : G -1-1-onto-> P <-> ( g e. G |-> ( 2nd ` g ) ) : G -1-1-onto-> P ) )
8	4 6 7	spcedv	|- ( V e. W -> E. f f : G -1-1-onto-> P )