Metamath Proof Explorer


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 )