Definition df-rest 11904

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

Assertion

Ref	Expression
df-rest	⊢ ↾t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥)))

Distinct variable group:   𝑥,𝑗,𝑦

Detailed syntax breakdown of Definition df-rest

Step	Hyp	Ref	Expression
1		crest 11902	. 2 class ↾t
2		vj	. . 3 setvar 𝑗
3		vx	. . 3 setvar 𝑥
4		cvv 2641	. . 3 class V
5		vy	. . . . 5 setvar 𝑦
6	2	cv 1298	. . . . 5 class 𝑗
7	5	cv 1298	. . . . . 6 class 𝑦
8	3	cv 1298	. . . . . 6 class 𝑥
9	7, 8	cin 3020	. . . . 5 class (𝑦 ∩ 𝑥)
10	5, 6, 9	cmpt 3929	. . . 4 class (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥))
11	10	crn 4478	. . 3 class ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥))
12	2, 3, 4, 4, 11	cmpo 5708	. 2 class (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥)))
13	1, 12	wceq 1299	1 wff ↾t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥)))

This definition is referenced by:  restfn  11906  restval  11908  restsspw  11912  restrcl  12118  ssrest  12133