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