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	⊢ ( 𝜑 → 𝐽 ∈ Top )
	restcls2.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
	restcls2.3	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
	restcls2.4	⊢ ( 𝜑 → 𝐾 = ( 𝐽 ↾t 𝑌 ) )
	restcls2.5	⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐾 ) )
Assertion	restcls2	⊢ ( 𝜑 → 𝑆 = ( ( ( 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	4	fveq2d	⊢ ( 𝜑 → ( cls ‘ 𝐾 ) = ( cls ‘ ( 𝐽 ↾t 𝑌 ) ) )
7	6	fveq1d	⊢ ( 𝜑 → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( ( cls ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ 𝑆 ) )
8		cldcls	⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐾 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = 𝑆 )
9	5 8	syl	⊢ ( 𝜑 → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = 𝑆 )
10	3 2	sseqtrd	⊢ ( 𝜑 → 𝑌 ⊆ ∪ 𝐽 )
11	1 2 3 4 5	restcls2lem	⊢ ( 𝜑 → 𝑆 ⊆ 𝑌 )
12		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
13		eqid	⊢ ( 𝐽 ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 )
14	12 13	restcls	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ ∪ 𝐽 ∧ 𝑆 ⊆ 𝑌 ) → ( ( cls ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ 𝑆 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )
15	1 10 11 14	syl3anc	⊢ ( 𝜑 → ( ( cls ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ 𝑆 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )
16	7 9 15	3eqtr3d	⊢ ( 𝜑 → 𝑆 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )