This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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