Theorem fvrnressn

Description: If the value of a function is in the range of the function restricted to the singleton containing the argument, then the value of the function is in the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018)

	Ref	Expression
Assertion	fvrnressn	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝐹 ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐹 “ { 𝑋 } ) = ran ( 𝐹 ↾ { 𝑋 } )
2	1	eleq2i	⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ { 𝑋 } ) ↔ ( 𝐹 ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) )
3		opeq1	⊢ ( 𝑥 = 𝑋 → ⟨ 𝑥 , ( 𝐹 ‘ 𝑋 ) ⟩ = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ )
4	3	eleq1d	⊢ ( 𝑥 = 𝑋 → ( ⟨ 𝑥 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ↔ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ) )
5	4	spcegv	⊢ ( 𝑋 ∈ 𝑉 → ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 → ∃ 𝑥 ⟨ 𝑥 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ) )
6		fvex	⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
7		elimasng	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝑋 ) ∈ V ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ { 𝑋 } ) ↔ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ) )
8	6 7	mpan2	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ { 𝑋 } ) ↔ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ) )
9		elrn2g	⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ V → ( ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 ↔ ∃ 𝑥 ⟨ 𝑥 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ) )
10	6 9	mp1i	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 ↔ ∃ 𝑥 ⟨ 𝑥 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ) )
11	5 8 10	3imtr4d	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ { 𝑋 } ) → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 ) )
12	2 11	syl5bir	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝐹 ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 ) )