This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem restfn

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

Ref Expression
Assertion restfn ⊢ ↾ 𝑡 Fn V × V

Proof

Step Hyp Ref Expression
1 df-rest ⊢ ↾ 𝑡 = j ∈ V , x ∈ V ⟼ ran ⁡ y ∈ j ⟼ y ∩ x
2 vex ⊢ j ∈ V
3 2 mptex ⊢ y ∈ j ⟼ y ∩ x ∈ V
4 3 rnex ⊢ ran ⁡ y ∈ j ⟼ y ∩ x ∈ V
5 1 4 fnmpoi ⊢ ↾ 𝑡 Fn V × V