Metamath Proof Explorer

Theorem restcldr

Description: A set which is closed in the subspace topology induced by a closed set is closed in the original topology. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion restcldr ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J ↾ 𝑡 A → B ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 cldrcl ⊢ A ∈ Clsd ⁡ J → J ∈ Top
2 eqid ⊢ ⋃ J = ⋃ J
3 2 cldss ⊢ A ∈ Clsd ⁡ J → A ⊆ ⋃ J
4 2 restcld ⊢ J ∈ Top ∧ A ⊆ ⋃ J → B ∈ Clsd ⁡ J ↾ 𝑡 A ↔ ∃ v ∈ Clsd ⁡ J B = v ∩ A
5 1 3 4 syl2anc ⊢ A ∈ Clsd ⁡ J → B ∈ Clsd ⁡ J ↾ 𝑡 A ↔ ∃ v ∈ Clsd ⁡ J B = v ∩ A
6 incld ⊢ v ∈ Clsd ⁡ J ∧ A ∈ Clsd ⁡ J → v ∩ A ∈ Clsd ⁡ J
7 6 ancoms ⊢ A ∈ Clsd ⁡ J ∧ v ∈ Clsd ⁡ J → v ∩ A ∈ Clsd ⁡ J
8 eleq1 ⊢ B = v ∩ A → B ∈ Clsd ⁡ J ↔ v ∩ A ∈ Clsd ⁡ J
9 7 8 syl5ibrcom ⊢ A ∈ Clsd ⁡ J ∧ v ∈ Clsd ⁡ J → B = v ∩ A → B ∈ Clsd ⁡ J
10 9 rexlimdva ⊢ A ∈ Clsd ⁡ J → ∃ v ∈ Clsd ⁡ J B = v ∩ A → B ∈ Clsd ⁡ J
11 5 10 sylbid ⊢ A ∈ Clsd ⁡ J → B ∈ Clsd ⁡ J ↾ 𝑡 A → B ∈ Clsd ⁡ J
12 11 imp ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J ↾ 𝑡 A → B ∈ Clsd ⁡ J