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 φJTop
restcls2.2 φX=J
restcls2.3 φYX
restcls2.4 φK=J𝑡Y
restcls2.5 φSClsdK
Assertion restcls2lem φSY

Proof

Step Hyp Ref Expression
1 restcls2.1 φJTop
2 restcls2.2 φX=J
3 restcls2.3 φYX
4 restcls2.4 φK=J𝑡Y
5 restcls2.5 φSClsdK
6 eqid K=K
7 6 cldss SClsdKSK
8 5 7 syl φSK
9 3 2 sseqtrd φYJ
10 eqid J=J
11 10 restuni JTopYJY=J𝑡Y
12 1 9 11 syl2anc φY=J𝑡Y
13 4 unieqd φK=J𝑡Y
14 12 13 eqtr4d φY=K
15 8 14 sseqtrrd φSY