Metamath Proof Explorer


Theorem restclssep

Description: Two disjoint closed sets in a subspace topology are separated in the original topology. (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
restclsseplem.6 φ S T =
restclssep.7 φ T Clsd K
Assertion restclssep φ S cls J T = cls J S T =

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 restclsseplem.6 φ S T =
7 restclssep.7 φ T Clsd K
8 incom cls J T S = S cls J T
9 incom S T = T S
10 9 6 eqtr3id φ T S =
11 1 2 3 4 5 restcls2lem φ S Y
12 1 2 3 4 7 10 11 restclsseplem φ cls J T S =
13 8 12 eqtr3id φ S cls J T =
14 1 2 3 4 7 restcls2lem φ T Y
15 1 2 3 4 5 6 14 restclsseplem φ cls J S T =
16 13 15 jca φ S cls J T = cls J S T =