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 ⊢ J ∈ V ∧ A ∈ W → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A

Proof

Step Hyp Ref Expression
1 elex ⊢ J ∈ V → J ∈ V
2 elex ⊢ A ∈ W → A ∈ V
3 mptexg ⊢ J ∈ V → x ∈ J ⟼ x ∩ A ∈ V
4 rnexg ⊢ x ∈ J ⟼ x ∩ A ∈ V → ran ⁡ x ∈ J ⟼ x ∩ A ∈ V
5 3 4 syl ⊢ J ∈ V → ran ⁡ x ∈ J ⟼ x ∩ A ∈ V
6 5 adantr ⊢ J ∈ V ∧ A ∈ V → ran ⁡ x ∈ J ⟼ x ∩ A ∈ V
7 simpl ⊢ j = J ∧ y = A → j = J
8 simpr ⊢ j = J ∧ y = A → y = A
9 8 ineq2d ⊢ j = J ∧ y = A → x ∩ y = x ∩ A
10 7 9 mpteq12dv ⊢ j = J ∧ y = A → x ∈ j ⟼ x ∩ y = x ∈ J ⟼ x ∩ A
11 10 rneqd ⊢ j = J ∧ y = A → ran ⁡ x ∈ j ⟼ x ∩ y = ran ⁡ x ∈ J ⟼ x ∩ A
12 df-rest ⊢ ↾ 𝑡 = j ∈ V , y ∈ V ⟼ ran ⁡ x ∈ j ⟼ x ∩ y
13 11 12 ovmpoga ⊢ J ∈ V ∧ A ∈ V ∧ ran ⁡ x ∈ J ⟼ x ∩ A ∈ V → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A
14 6 13 mpd3an3 ⊢ J ∈ V ∧ A ∈ V → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A
15 1 2 14 syl2an ⊢ J ∈ V ∧ A ∈ W → J ↾ 𝑡 A = ran ⁡ x ∈ J ⟼ x ∩ A