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