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 ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∩ I ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑥 } )

Proof

Step Hyp Ref Expression
1 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
2 1 ineq1d ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ∩ I ) = ( 𝐹 ∩ I ) )
3 inres ⊢ ( I ∩ ( 𝐹 ↾ 𝐴 ) ) = ( ( I ∩ 𝐹 ) ↾ 𝐴 )
4 incom ⊢ ( I ∩ 𝐹 ) = ( 𝐹 ∩ I )
5 4 reseq1i ⊢ ( ( I ∩ 𝐹 ) ↾ 𝐴 ) = ( ( 𝐹 ∩ I ) ↾ 𝐴 )
6 3 5 eqtri ⊢ ( I ∩ ( 𝐹 ↾ 𝐴 ) ) = ( ( 𝐹 ∩ I ) ↾ 𝐴 )
7 incom ⊢ ( ( 𝐹 ↾ 𝐴 ) ∩ I ) = ( I ∩ ( 𝐹 ↾ 𝐴 ) )
8 inres ⊢ ( 𝐹 ∩ ( I ↾ 𝐴 ) ) = ( ( 𝐹 ∩ I ) ↾ 𝐴 )
9 6 7 8 3eqtr4i ⊢ ( ( 𝐹 ↾ 𝐴 ) ∩ I ) = ( 𝐹 ∩ ( I ↾ 𝐴 ) )
10 2 9 eqtr3di ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ∩ I ) = ( 𝐹 ∩ ( I ↾ 𝐴 ) ) )
11 10 dmeqd ⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∩ I ) = dom ( 𝐹 ∩ ( I ↾ 𝐴 ) ) )
12 fnresi ⊢ ( I ↾ 𝐴 ) Fn 𝐴
13 fndmin ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴 ) Fn 𝐴 ) → dom ( 𝐹 ∩ ( I ↾ 𝐴 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) } )
14 12 13 mpan2 ⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∩ ( I ↾ 𝐴 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) } )
15 fvresi ⊢ ( 𝑥 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
16 15 eqeq2d ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
17 16 rabbiia ⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑥 }
18 17 a1i ⊢ ( 𝐹 Fn 𝐴 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑥 } )
19 11 14 18 3eqtrd ⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∩ I ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑥 } )