Theorem restcls2

Description: A closed set in a subspace topology is the closure in the original topology intersecting with 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	restcls2	|- ( ph -> S = ( ( ( cls ` J ) ` S ) i^i 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	4	fveq2d	|- ( ph -> ( cls ` K ) = ( cls ` ( J |`t Y ) ) )
7	6	fveq1d	|- ( ph -> ( ( cls ` K ) ` S ) = ( ( cls ` ( J |`t Y ) ) ` S ) )
8		cldcls	|- ( S e. ( Clsd ` K ) -> ( ( cls ` K ) ` S ) = S )
9	5 8	syl	|- ( ph -> ( ( cls ` K ) ` S ) = S )
10	3 2	sseqtrd	|- ( ph -> Y C_ U. J )
11	1 2 3 4 5	restcls2lem	|- ( ph -> S C_ Y )
12		eqid	|- U. J = U. J
13		eqid	|- ( J |`t Y ) = ( J |`t Y )
14	12 13	restcls	|- ( ( J e. Top /\ Y C_ U. J /\ S C_ Y ) -> ( ( cls ` ( J |`t Y ) ) ` S ) = ( ( ( cls ` J ) ` S ) i^i Y ) )
15	1 10 11 14	syl3anc	|- ( ph -> ( ( cls ` ( J |`t Y ) ) ` S ) = ( ( ( cls ` J ) ` S ) i^i Y ) )
16	7 9 15	3eqtr3d	|- ( ph -> S = ( ( ( cls ` J ) ` S ) i^i Y ) )