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 ↾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 ( 𝑦 ∈ 𝑗 ↦ ( 𝑦 ∩ 𝑥 ) ) )