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	⊢ ( 𝜑 → 𝐽 ∈ Top )
	restcls2.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
	restcls2.3	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
	restcls2.4	⊢ ( 𝜑 → 𝐾 = ( 𝐽 ↾t 𝑌 ) )
	restcls2.5	⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐾 ) )
	restclsseplem.6	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
	restclssep.7	⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐾 ) )
Assertion	restclssep	⊢ ( 𝜑 → ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		restcls2.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		restcls2.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
3		restcls2.3	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
4		restcls2.4	⊢ ( 𝜑 → 𝐾 = ( 𝐽 ↾t 𝑌 ) )
5		restcls2.5	⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐾 ) )
6		restclsseplem.6	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
7		restclssep.7	⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐾 ) )
8		incom	⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∩ 𝑆 ) = ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) )
9		incom	⊢ ( 𝑆 ∩ 𝑇 ) = ( 𝑇 ∩ 𝑆 )
10	9 6	eqtr3id	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑆 ) = ∅ )
11	1 2 3 4 5	restcls2lem	⊢ ( 𝜑 → 𝑆 ⊆ 𝑌 )
12	1 2 3 4 7 10 11	restclsseplem	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∩ 𝑆 ) = ∅ )
13	8 12	eqtr3id	⊢ ( 𝜑 → ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ )
14	1 2 3 4 7	restcls2lem	⊢ ( 𝜑 → 𝑇 ⊆ 𝑌 )
15	1 2 3 4 5 6 14	restclsseplem	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ )
16	13 15	jca	⊢ ( 𝜑 → ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) )