Theorem restcls2lem

Description: A closed set in a subspace topology is a subset of 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	restcls2lem	⊢ ( 𝜑 → 𝑆 ⊆ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		restcls2.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		restcls2.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
3		restcls2.3	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
4		restcls2.4	⊢ ( 𝜑 → 𝐾 = ( 𝐽 ↾t 𝑌 ) )
5		restcls2.5	⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐾 ) )
6		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
7	6	cldss	⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐾 ) → 𝑆 ⊆ ∪ 𝐾 )
8	5 7	syl	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐾 )
9	3 2	sseqtrd	⊢ ( 𝜑 → 𝑌 ⊆ ∪ 𝐽 )
10		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
11	10	restuni	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ ∪ 𝐽 ) → 𝑌 = ∪ ( 𝐽 ↾t 𝑌 ) )
12	1 9 11	syl2anc	⊢ ( 𝜑 → 𝑌 = ∪ ( 𝐽 ↾t 𝑌 ) )
13	4	unieqd	⊢ ( 𝜑 → ∪ 𝐾 = ∪ ( 𝐽 ↾t 𝑌 ) )
14	12 13	eqtr4d	⊢ ( 𝜑 → 𝑌 = ∪ 𝐾 )
15	8 14	sseqtrrd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑌 )