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 ⊢ X = ⋃ J
Assertion restin ⊢ J ∈ V ∧ A ∈ W → J ↾ 𝑡 A = J ↾ 𝑡 A ∩ X

Proof

Step Hyp Ref Expression
1 restin.1 ⊢ X = ⋃ J
2 uniexg ⊢ J ∈ V → ⋃ J ∈ V
3 1 2 eqeltrid ⊢ J ∈ V → X ∈ V
4 3 adantr ⊢ J ∈ V ∧ A ∈ W → X ∈ V
5 restco ⊢ J ∈ V ∧ X ∈ V ∧ A ∈ W → J ↾ 𝑡 X ↾ 𝑡 A = J ↾ 𝑡 X ∩ A
6 5 3com23 ⊢ J ∈ V ∧ A ∈ W ∧ X ∈ V → J ↾ 𝑡 X ↾ 𝑡 A = J ↾ 𝑡 X ∩ A
7 4 6 mpd3an3 ⊢ J ∈ V ∧ A ∈ W → J ↾ 𝑡 X ↾ 𝑡 A = J ↾ 𝑡 X ∩ A
8 1 restid ⊢ J ∈ V → J ↾ 𝑡 X = J
9 8 adantr ⊢ J ∈ V ∧ A ∈ W → J ↾ 𝑡 X = J
10 9 oveq1d ⊢ J ∈ V ∧ A ∈ W → J ↾ 𝑡 X ↾ 𝑡 A = J ↾ 𝑡 A
11 incom ⊢ X ∩ A = A ∩ X
12 11 oveq2i ⊢ J ↾ 𝑡 X ∩ A = J ↾ 𝑡 A ∩ X
13 12 a1i ⊢ J ∈ V ∧ A ∈ W → J ↾ 𝑡 X ∩ A = J ↾ 𝑡 A ∩ X
14 7 10 13 3eqtr3d ⊢ J ∈ V ∧ A ∈ W → J ↾ 𝑡 A = J ↾ 𝑡 A ∩ X