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 X=J
Assertion restcldi AXBClsdJBABClsdJ𝑡A

Proof

Step Hyp Ref Expression
1 restcldi.1 X=J
2 simp2 AXBClsdJBABClsdJ
3 dfss BAB=BA
4 3 biimpi BAB=BA
5 4 3ad2ant3 AXBClsdJBAB=BA
6 ineq1 v=BvA=BA
7 6 rspceeqv BClsdJB=BAvClsdJB=vA
8 2 5 7 syl2anc AXBClsdJBAvClsdJB=vA
9 cldrcl BClsdJJTop
10 9 3ad2ant2 AXBClsdJBAJTop
11 simp1 AXBClsdJBAAX
12 1 restcld JTopAXBClsdJ𝑡AvClsdJB=vA
13 10 11 12 syl2anc AXBClsdJBABClsdJ𝑡AvClsdJB=vA
14 8 13 mpbird AXBClsdJBABClsdJ𝑡A