Theorem fnelfp

Description: Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	fnelfp	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fninfp	⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∩ I ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑥 } )
2	1	eleq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ dom ( 𝐹 ∩ I ) ↔ 𝑋 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑥 } ) )
3		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
4		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
5	3 4	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ↔ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )
6	5	elrab3	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑥 } ↔ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )
7	2 6	sylan9bb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )