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

Metamath Proof Explorer

Definition df-rest

Description: Function returning the subspace topology induced by the topology y and the set x . (Contributed by FL, 20-Sep-2010) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion df-rest ⊢ ↾ 𝑡 = j ∈ V , x ∈ V ⟼ ran ⁡ y ∈ j ⟼ y ∩ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 crest class ↾ 𝑡
1 vj setvar j
2 cvv class V
3 vx setvar x
4 vy setvar y
5 1 cv setvar j
6 4 cv setvar y
7 3 cv setvar x
8 6 7 cin class y ∩ x
9 4 5 8 cmpt class y ∈ j ⟼ y ∩ x
10 9 crn class ran ⁡ y ∈ j ⟼ y ∩ x
11 1 3 2 2 10 cmpo class j ∈ V , x ∈ V ⟼ ran ⁡ y ∈ j ⟼ y ∩ x
12 0 11 wceq wff ↾ 𝑡 = j ∈ V , x ∈ V ⟼ ran ⁡ y ∈ j ⟼ y ∩ x