Metamath Proof Explorer


Theorem fninfp

Description: Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion fninfp
|- ( F Fn A -> dom ( F i^i _I ) = { x e. A | ( F ` x ) = x } )

Proof

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