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

Metamath Proof Explorer

Theorem restval

Description: The subspace topology induced by the topology J on the set A . (Contributed by FL, 20-Sep-2010) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion restval ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐽 ∈ 𝑉 → 𝐽 ∈ V )
2 elex ⊢ ( 𝐴 ∈ 𝑊 → 𝐴 ∈ V )
3 mptexg ⊢ ( 𝐽 ∈ V → ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) ∈ V )
4 rnexg ⊢ ( ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) ∈ V → ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) ∈ V )
5 3 4 syl ⊢ ( 𝐽 ∈ V → ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) ∈ V )
6 5 adantr ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) ∈ V )
7 simpl ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑦 = 𝐴 ) → 𝑗 = 𝐽 )
8 simpr ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑦 = 𝐴 ) → 𝑦 = 𝐴 )
9 8 ineq2d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑦 = 𝐴 ) → ( 𝑥 ∩ 𝑦 ) = ( 𝑥 ∩ 𝐴 ) )
10 7 9 mpteq12dv ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑦 = 𝐴 ) → ( 𝑥 ∈ 𝑗 ↦ ( 𝑥 ∩ 𝑦 ) ) = ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
11 10 rneqd ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑦 = 𝐴 ) → ran ( 𝑥 ∈ 𝑗 ↦ ( 𝑥 ∩ 𝑦 ) ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
12 df-rest ⊢ ↾t = ( 𝑗 ∈ V , 𝑦 ∈ V ↦ ran ( 𝑥 ∈ 𝑗 ↦ ( 𝑥 ∩ 𝑦 ) ) )
13 11 12 ovmpoga ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ∧ ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) ∈ V ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
14 6 13 mpd3an3 ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
15 1 2 14 syl2an ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )