Description: The set G of the "simple pseudographs" with a fixed set of vertices V and the class P of subsets of the set of pairs over the fixed set V are equinumerous. (Contributed by AV, 27-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 | uspgrspren | |- ( V e. W -> G ~~ 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 | 1 2 | uspgrbispr | |- ( V e. W -> E. f f : G -1-1-onto-> P ) |
4 | bren | |- ( G ~~ P <-> E. f f : G -1-1-onto-> P ) |
|
5 | 3 4 | sylibr | |- ( V e. W -> G ~~ P ) |