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

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 ( ( 𝐴 ∈ ( 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 ‘ 𝐽 ) )