Theorem restfn

Description: The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015)

	Ref	Expression
Assertion	restfn	⊢ ↾t Fn ( V × V )

Proof

Step	Hyp	Ref	Expression
1		df-rest	⊢ ↾t = ( 𝑗 ∈ V , 𝑥 ∈ V ↦ ran ( 𝑦 ∈ 𝑗 ↦ ( 𝑦 ∩ 𝑥 ) ) )
2		vex	⊢ 𝑗 ∈ V
3	2	mptex	⊢ ( 𝑦 ∈ 𝑗 ↦ ( 𝑦 ∩ 𝑥 ) ) ∈ V
4	3	rnex	⊢ ran ( 𝑦 ∈ 𝑗 ↦ ( 𝑦 ∩ 𝑥 ) ) ∈ V
5	1 4	fnmpoi	⊢ ↾t Fn ( V × V )