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 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑥 } )