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