# 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 ( 𝑥𝐽 ↦ ( 𝑥𝐴 ) ) )