Theorem restin

Description: When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Hypothesis	restin.1	⊢ 𝑋 = ∪ 𝐽
Assertion	restin	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		restin.1	⊢ 𝑋 = ∪ 𝐽
2		uniexg	⊢ ( 𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V )
3	1 2	eqeltrid	⊢ ( 𝐽 ∈ 𝑉 → 𝑋 ∈ V )
4	3	adantr	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → 𝑋 ∈ V )
5		restco	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝑋 ∈ V ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝐽 ↾t 𝑋 ) ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) )
6	5	3com23	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑋 ∈ V ) → ( ( 𝐽 ↾t 𝑋 ) ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) )
7	4 6	mpd3an3	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝐽 ↾t 𝑋 ) ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) )
8	1	restid	⊢ ( 𝐽 ∈ 𝑉 → ( 𝐽 ↾t 𝑋 ) = 𝐽 )
9	8	adantr	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t 𝑋 ) = 𝐽 )
10	9	oveq1d	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝐽 ↾t 𝑋 ) ↾t 𝐴 ) = ( 𝐽 ↾t 𝐴 ) )
11		incom	⊢ ( 𝑋 ∩ 𝐴 ) = ( 𝐴 ∩ 𝑋 )
12	11	oveq2i	⊢ ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) )
13	12	a1i	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) )
14	7 10 13	3eqtr3d	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) )