Metamath Proof Explorer

Theorem cnvf1o

Description: Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014)

Ref Expression
Assertion cnvf1o 
|- ( Rel A -> ( x e. A |-> U. `' { x } ) : A -1-1-onto-> `' A )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. A |-> U. `' { x } ) = ( x e. A |-> U. `' { x } )
2 snex 
 |-  { x } e. _V
3 2 cnvex 
 |-  `' { x } e. _V
4 3 uniex 
 |-  U. `' { x } e. _V
5 4 a1i 
 |-  ( ( Rel A /\ x e. A ) -> U. `' { x } e. _V )
6 snex 
 |-  { y } e. _V
7 6 cnvex 
 |-  `' { y } e. _V
8 7 uniex 
 |-  U. `' { y } e. _V
9 8 a1i 
 |-  ( ( Rel A /\ y e. `' A ) -> U. `' { y } e. _V )
10 cnvf1olem 
 |-  ( ( Rel A /\ ( x e. A /\ y = U. `' { x } ) ) -> ( y e. `' A /\ x = U. `' { y } ) )
11 relcnv 
 |-  Rel `' A
12 simpr 
 |-  ( ( Rel A /\ ( y e. `' A /\ x = U. `' { y } ) ) -> ( y e. `' A /\ x = U. `' { y } ) )
13 cnvf1olem 
 |-  ( ( Rel `' A /\ ( y e. `' A /\ x = U. `' { y } ) ) -> ( x e. `' `' A /\ y = U. `' { x } ) )
14 11 12 13 sylancr 
 |-  ( ( Rel A /\ ( y e. `' A /\ x = U. `' { y } ) ) -> ( x e. `' `' A /\ y = U. `' { x } ) )
15 dfrel2 
 |-  ( Rel A <-> `' `' A = A )
16 eleq2 
 |-  ( `' `' A = A -> ( x e. `' `' A <-> x e. A ) )
17 15 16 sylbi 
 |-  ( Rel A -> ( x e. `' `' A <-> x e. A ) )
18 17 anbi1d 
 |-  ( Rel A -> ( ( x e. `' `' A /\ y = U. `' { x } ) <-> ( x e. A /\ y = U. `' { x } ) ) )
19 18 adantr 
 |-  ( ( Rel A /\ ( y e. `' A /\ x = U. `' { y } ) ) -> ( ( x e. `' `' A /\ y = U. `' { x } ) <-> ( x e. A /\ y = U. `' { x } ) ) )
20 14 19 mpbid 
 |-  ( ( Rel A /\ ( y e. `' A /\ x = U. `' { y } ) ) -> ( x e. A /\ y = U. `' { x } ) )
21 10 20 impbida 
 |-  ( Rel A -> ( ( x e. A /\ y = U. `' { x } ) <-> ( y e. `' A /\ x = U. `' { y } ) ) )
22 1 5 9 21 f1od 
 |-  ( Rel A -> ( x e. A |-> U. `' { x } ) : A -1-1-onto-> `' A )