Theorem restclssep

Description: Two disjoint closed sets in a subspace topology are separated in the original topology. (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 ) )
	restclsseplem.6	|- ( ph -> ( S i^i T ) = (/) )
	restclssep.7	|- ( ph -> T e. ( Clsd ` K ) )
Assertion	restclssep	|- ( ph -> ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) )

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		restclsseplem.6	|- ( ph -> ( S i^i T ) = (/) )
7		restclssep.7	|- ( ph -> T e. ( Clsd ` K ) )
8		incom	|- ( ( ( cls ` J ) ` T ) i^i S ) = ( S i^i ( ( cls ` J ) ` T ) )
9		incom	|- ( S i^i T ) = ( T i^i S )
10	9 6	eqtr3id	|- ( ph -> ( T i^i S ) = (/) )
11	1 2 3 4 5	restcls2lem	|- ( ph -> S C_ Y )
12	1 2 3 4 7 10 11	restclsseplem	|- ( ph -> ( ( ( cls ` J ) ` T ) i^i S ) = (/) )
13	8 12	eqtr3id	|- ( ph -> ( S i^i ( ( cls ` J ) ` T ) ) = (/) )
14	1 2 3 4 7	restcls2lem	|- ( ph -> T C_ Y )
15	1 2 3 4 5 6 14	restclsseplem	|- ( ph -> ( ( ( cls ` J ) ` S ) i^i T ) = (/) )
16	13 15	jca	|- ( ph -> ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) )