Metamath Proof Explorer

Theorem restcldi

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

Ref Expression
Hypothesis restcldi.1 ⊢ X = ⋃ J
Assertion restcldi ⊢ A ⊆ X ∧ B ∈ Clsd ⁡ J ∧ B ⊆ A → B ∈ Clsd ⁡ J ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 restcldi.1 ⊢ X = ⋃ J
2 simp2 ⊢ A ⊆ X ∧ B ∈ Clsd ⁡ J ∧ B ⊆ A → B ∈ Clsd ⁡ J
3 dfss ⊢ B ⊆ A ↔ B = B ∩ A
4 3 biimpi ⊢ B ⊆ A → B = B ∩ A
5 4 3ad2ant3 ⊢ A ⊆ X ∧ B ∈ Clsd ⁡ J ∧ B ⊆ A → B = B ∩ A
6 ineq1 ⊢ v = B → v ∩ A = B ∩ A
7 6 rspceeqv ⊢ B ∈ Clsd ⁡ J ∧ B = B ∩ A → ∃ v ∈ Clsd ⁡ J B = v ∩ A
8 2 5 7 syl2anc ⊢ A ⊆ X ∧ B ∈ Clsd ⁡ J ∧ B ⊆ A → ∃ v ∈ Clsd ⁡ J B = v ∩ A
9 cldrcl ⊢ B ∈ Clsd ⁡ J → J ∈ Top
10 9 3ad2ant2 ⊢ A ⊆ X ∧ B ∈ Clsd ⁡ J ∧ B ⊆ A → J ∈ Top
11 simp1 ⊢ A ⊆ X ∧ B ∈ Clsd ⁡ J ∧ B ⊆ A → A ⊆ X
12 1 restcld ⊢ J ∈ Top ∧ A ⊆ X → B ∈ Clsd ⁡ J ↾ 𝑡 A ↔ ∃ v ∈ Clsd ⁡ J B = v ∩ A
13 10 11 12 syl2anc ⊢ A ⊆ X ∧ B ∈ Clsd ⁡ J ∧ B ⊆ A → B ∈ Clsd ⁡ J ↾ 𝑡 A ↔ ∃ v ∈ Clsd ⁡ J B = v ∩ A
14 8 13 mpbird ⊢ A ⊆ X ∧ B ∈ Clsd ⁡ J ∧ B ⊆ A → B ∈ Clsd ⁡ J ↾ 𝑡 A