# 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 ${⊢}{↾}_{𝑡}=\left({j}\in \mathrm{V},{x}\in \mathrm{V}⟼\mathrm{ran}\left({y}\in {j}⟼{y}\cap {x}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 crest ${class}{↾}_{𝑡}$
1 vj ${setvar}{j}$
2 cvv ${class}\mathrm{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}\left({y}\cap {x}\right)$
9 4 5 8 cmpt ${class}\left({y}\in {j}⟼{y}\cap {x}\right)$
10 9 crn ${class}\mathrm{ran}\left({y}\in {j}⟼{y}\cap {x}\right)$
11 1 3 2 2 10 cmpo ${class}\left({j}\in \mathrm{V},{x}\in \mathrm{V}⟼\mathrm{ran}\left({y}\in {j}⟼{y}\cap {x}\right)\right)$
12 0 11 wceq ${wff}{↾}_{𝑡}=\left({j}\in \mathrm{V},{x}\in \mathrm{V}⟼\mathrm{ran}\left({y}\in {j}⟼{y}\cap {x}\right)\right)$