Metamath Proof Explorer


Theorem restcls2

Description: A closed set in a subspace topology is the closure in the original topology intersecting with the subspace. (Contributed by Zhi Wang, 2-Sep-2024)

Ref Expression
Hypotheses restcls2.1 φ J Top
restcls2.2 φ X = J
restcls2.3 φ Y X
restcls2.4 φ K = J 𝑡 Y
restcls2.5 φ S Clsd K
Assertion restcls2 φ S = cls J S Y

Proof

Step Hyp Ref Expression
1 restcls2.1 φ J Top
2 restcls2.2 φ X = J
3 restcls2.3 φ Y X
4 restcls2.4 φ K = J 𝑡 Y
5 restcls2.5 φ S Clsd K
6 4 fveq2d φ cls K = cls J 𝑡 Y
7 6 fveq1d φ cls K S = cls J 𝑡 Y S
8 cldcls S Clsd K cls K S = S
9 5 8 syl φ cls K S = S
10 3 2 sseqtrd φ Y J
11 1 2 3 4 5 restcls2lem φ S Y
12 eqid J = J
13 eqid J 𝑡 Y = J 𝑡 Y
14 12 13 restcls J Top Y J S Y cls J 𝑡 Y S = cls J S Y
15 1 10 11 14 syl3anc φ cls J 𝑡 Y S = cls J S Y
16 7 9 15 3eqtr3d φ S = cls J S Y