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 𝐴 ) ) )