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	|- ( ph -> J e. Top )
	restcls2.2	|- ( ph -> X = U. J )
	restcls2.3	|- ( ph -> Y C_ X )
	restcls2.4	|- ( ph -> K = ( J |`t Y ) )
	restcls2.5	|- ( ph -> S e. ( Clsd ` K ) )
Assertion	restcls2lem	|- ( ph -> S C_ Y )

Proof

Step	Hyp	Ref	Expression
1		restcls2.1	|- ( ph -> J e. Top )
2		restcls2.2	|- ( ph -> X = U. J )
3		restcls2.3	|- ( ph -> Y C_ X )
4		restcls2.4	|- ( ph -> K = ( J |`t Y ) )
5		restcls2.5	|- ( ph -> S e. ( Clsd ` K ) )
6		eqid	|- U. K = U. K
7	6	cldss	|- ( S e. ( Clsd ` K ) -> S C_ U. K )
8	5 7	syl	|- ( ph -> S C_ U. K )
9	3 2	sseqtrd	|- ( ph -> Y C_ U. J )
10		eqid	|- U. J = U. J
11	10	restuni	|- ( ( J e. Top /\ Y C_ U. J ) -> Y = U. ( J |`t Y ) )
12	1 9 11	syl2anc	|- ( ph -> Y = U. ( J |`t Y ) )
13	4	unieqd	|- ( ph -> U. K = U. ( J |`t Y ) )
14	12 13	eqtr4d	|- ( ph -> Y = U. K )
15	8 14	sseqtrrd	|- ( ph -> S C_ Y )