Step |
Hyp |
Ref |
Expression |
1 |
|
fnresdm |
|- ( F Fn A -> ( F |` A ) = F ) |
2 |
1
|
ineq1d |
|- ( F Fn A -> ( ( F |` A ) i^i _I ) = ( F i^i _I ) ) |
3 |
|
inres |
|- ( _I i^i ( F |` A ) ) = ( ( _I i^i F ) |` A ) |
4 |
|
incom |
|- ( _I i^i F ) = ( F i^i _I ) |
5 |
4
|
reseq1i |
|- ( ( _I i^i F ) |` A ) = ( ( F i^i _I ) |` A ) |
6 |
3 5
|
eqtri |
|- ( _I i^i ( F |` A ) ) = ( ( F i^i _I ) |` A ) |
7 |
|
incom |
|- ( ( F |` A ) i^i _I ) = ( _I i^i ( F |` A ) ) |
8 |
|
inres |
|- ( F i^i ( _I |` A ) ) = ( ( F i^i _I ) |` A ) |
9 |
6 7 8
|
3eqtr4i |
|- ( ( F |` A ) i^i _I ) = ( F i^i ( _I |` A ) ) |
10 |
2 9
|
eqtr3di |
|- ( F Fn A -> ( F i^i _I ) = ( F i^i ( _I |` A ) ) ) |
11 |
10
|
dmeqd |
|- ( F Fn A -> dom ( F i^i _I ) = dom ( F i^i ( _I |` A ) ) ) |
12 |
|
fnresi |
|- ( _I |` A ) Fn A |
13 |
|
fndmin |
|- ( ( F Fn A /\ ( _I |` A ) Fn A ) -> dom ( F i^i ( _I |` A ) ) = { x e. A | ( F ` x ) = ( ( _I |` A ) ` x ) } ) |
14 |
12 13
|
mpan2 |
|- ( F Fn A -> dom ( F i^i ( _I |` A ) ) = { x e. A | ( F ` x ) = ( ( _I |` A ) ` x ) } ) |
15 |
|
fvresi |
|- ( x e. A -> ( ( _I |` A ) ` x ) = x ) |
16 |
15
|
eqeq2d |
|- ( x e. A -> ( ( F ` x ) = ( ( _I |` A ) ` x ) <-> ( F ` x ) = x ) ) |
17 |
16
|
rabbiia |
|- { x e. A | ( F ` x ) = ( ( _I |` A ) ` x ) } = { x e. A | ( F ` x ) = x } |
18 |
17
|
a1i |
|- ( F Fn A -> { x e. A | ( F ` x ) = ( ( _I |` A ) ` x ) } = { x e. A | ( F ` x ) = x } ) |
19 |
11 14 18
|
3eqtrd |
|- ( F Fn A -> dom ( F i^i _I ) = { x e. A | ( F ` x ) = x } ) |