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

Metamath Proof Explorer

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 ( 𝐴 ∩ 𝑋 ) ) )