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	⊢ ↾t = ( 𝑗 ∈ V , 𝑥 ∈ V ↦ ran ( 𝑦 ∈ 𝑗 ↦ ( 𝑦 ∩ 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crest	⊢ ↾t
1		vj	⊢ 𝑗
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5	1	cv	⊢ 𝑗
6	4	cv	⊢ 𝑦
7	3	cv	⊢ 𝑥
8	6 7	cin	⊢ ( 𝑦 ∩ 𝑥 )
9	4 5 8	cmpt	⊢ ( 𝑦 ∈ 𝑗 ↦ ( 𝑦 ∩ 𝑥 ) )
10	9	crn	⊢ ran ( 𝑦 ∈ 𝑗 ↦ ( 𝑦 ∩ 𝑥 ) )
11	1 3 2 2 10	cmpo	⊢ ( 𝑗 ∈ V , 𝑥 ∈ V ↦ ran ( 𝑦 ∈ 𝑗 ↦ ( 𝑦 ∩ 𝑥 ) ) )
12	0 11	wceq	⊢ ↾t = ( 𝑗 ∈ V , 𝑥 ∈ V ↦ ran ( 𝑦 ∈ 𝑗 ↦ ( 𝑦 ∩ 𝑥 ) ) )