Metamath Proof Explorer


Theorem uspgrsprf1o

Description: The mapping F 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 . See also the comments on uspgrbisymrel . (Contributed by AV, 25-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 uspgrsprf1o
|- ( V e. W -> 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 uspgrsprf.f
 |-  F = ( g e. G |-> ( 2nd ` g ) )
4 1 2 3 uspgrsprf1
 |-  F : G -1-1-> P
5 4 a1i
 |-  ( V e. W -> F : G -1-1-> P )
6 1 2 3 uspgrsprfo
 |-  ( V e. W -> F : G -onto-> P )
7 df-f1o
 |-  ( F : G -1-1-onto-> P <-> ( F : G -1-1-> P /\ F : G -onto-> P ) )
8 5 6 7 sylanbrc
 |-  ( V e. W -> F : G -1-1-onto-> P )