Metamath Proof Explorer


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 ( 𝜑𝑆𝑌 )