Theorem cnven

Description: A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Assertion	cnven	|- ( ( Rel A /\ A e. V ) -> A ~~ `' A )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( Rel A /\ A e. V ) -> A e. V )
2		cnvexg	|- ( A e. V -> `' A e. _V )
3	2	adantl	|- ( ( Rel A /\ A e. V ) -> `' A e. _V )
4		cnvf1o	|- ( Rel A -> ( x e. A |-> U. `' { x } ) : A -1-1-onto-> `' A )
5	4	adantr	|- ( ( Rel A /\ A e. V ) -> ( x e. A |-> U. `' { x } ) : A -1-1-onto-> `' A )
6		f1oen2g	|- ( ( A e. V /\ `' A e. _V /\ ( x e. A |-> U. `' { x } ) : A -1-1-onto-> `' A ) -> A ~~ `' A )
7	1 3 5 6	syl3anc	|- ( ( Rel A /\ A e. V ) -> A ~~ `' A )