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 ) |
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 ) |