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