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	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		cldrcl	⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
2		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
3	2	cldss	⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → 𝐴 ⊆ ∪ 𝐽 )
4	2	restcld	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ) → ( 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) ) )
5	1 3 4	syl2anc	⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → ( 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) ) )
6		incld	⊢ ( ( 𝑣 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑣 ∩ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )
7	6	ancoms	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑣 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑣 ∩ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )
8		eleq1	⊢ ( 𝐵 = ( 𝑣 ∩ 𝐴 ) → ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑣 ∩ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ) )
9	7 8	syl5ibrcom	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑣 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐵 = ( 𝑣 ∩ 𝐴 ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) )
10	9	rexlimdva	⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → ( ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) 𝐵 = ( 𝑣 ∩ 𝐴 ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) )
11	5 10	sylbid	⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → ( 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) )
12	11	imp	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )