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 )