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 φ J Top
restcls2.2 φ X = J
restcls2.3 φ Y X
restcls2.4 φ K = J 𝑡 Y
restcls2.5 φ S Clsd K
Assertion restcls2lem φ S Y

Proof

Step Hyp Ref Expression
1 restcls2.1 φ J Top
2 restcls2.2 φ X = J
3 restcls2.3 φ Y X
4 restcls2.4 φ K = J 𝑡 Y
5 restcls2.5 φ S Clsd K
6 eqid K = K
7 6 cldss S Clsd K S K
8 5 7 syl φ S K
9 3 2 sseqtrd φ Y J
10 eqid J = J
11 10 restuni J Top Y J Y = 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 φ S Y