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

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 ⊢ 𝑋 = ∪ 𝐽
Assertion restcldi ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 restcldi.1 ⊢ 𝑋 = ∪ 𝐽
2 simp2 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
3 dfss ⊢ ( 𝐵 ⊆ 𝐴 ↔ 𝐵 = ( 𝐵 ∩ 𝐴 ) )
4 3 biimpi ⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 = ( 𝐵 ∩ 𝐴 ) )
5 4 3ad2ant3 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 = ( 𝐵 ∩ 𝐴 ) )
6 ineq1 ⊢ ( 𝑣 = 𝐵 → ( 𝑣 ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )
7 6 rspceeqv ⊢ ( ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 = ( 𝐵 ∩ 𝐴 ) ) → ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) )
8 2 5 7 syl2anc ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) )
9 cldrcl ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
10 9 3ad2ant2 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐽 ∈ Top )
11 simp1 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐴 ⊆ 𝑋 )
12 1 restcld ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) ) )
13 10 11 12 syl2anc ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) ) )
14 8 13 mpbird ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) )