Theorem uspgrymrelen

Description: The set G of the "simple pseudographs" with a fixed set of vertices V and the class R of the symmetric relations on the fixed set V are equinumerous. For more details about the class G of all "simple pseudographs" see comments on uspgrbisymrel . (Contributed by AV, 27-Nov-2021)

	Ref	Expression
Hypotheses	uspgrbisymrel.g	|- G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
	uspgrbisymrel.r	|- R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
Assertion	uspgrymrelen	|- ( V e. W -> G ~~ R )

Proof

Step	Hyp	Ref	Expression
1		uspgrbisymrel.g	|- G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
2		uspgrbisymrel.r	|- R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
3		eqid	|- ~P ( Pairs ` V ) = ~P ( Pairs ` V )
4	3 1	uspgrspren	|- ( V e. W -> G ~~ ~P ( Pairs ` V ) )
5	3 2	sprsymrelen	|- ( V e. W -> ~P ( Pairs ` V ) ~~ R )
6		entr	|- ( ( G ~~ ~P ( Pairs ` V ) /\ ~P ( Pairs ` V ) ~~ R ) -> G ~~ R )
7	4 5 6	syl2anc	|- ( V e. W -> G ~~ R )