Theorem restclsseplem

Description: Lemma for restclssep . (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 ) = (/) )
	restclsseplem.7	|- ( ph -> T C_ Y )
Assertion	restclsseplem	|- ( ph -> ( ( ( 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		restclsseplem.7	|- ( ph -> T C_ Y )
8	1 2 3 4 5	restcls2	|- ( ph -> S = ( ( ( cls ` J ) ` S ) i^i Y ) )
9	8	ineq1d	|- ( ph -> ( S i^i T ) = ( ( ( ( cls ` J ) ` S ) i^i Y ) i^i T ) )
10		inass	|- ( ( ( ( cls ` J ) ` S ) i^i Y ) i^i T ) = ( ( ( cls ` J ) ` S ) i^i ( Y i^i T ) )
11	9 10	eqtrdi	|- ( ph -> ( S i^i T ) = ( ( ( cls ` J ) ` S ) i^i ( Y i^i T ) ) )
12		sseqin2	|- ( T C_ Y <-> ( Y i^i T ) = T )
13	7 12	sylib	|- ( ph -> ( Y i^i T ) = T )
14	13	ineq2d	|- ( ph -> ( ( ( cls ` J ) ` S ) i^i ( Y i^i T ) ) = ( ( ( cls ` J ) ` S ) i^i T ) )
15	11 6 14	3eqtr3rd	|- ( ph -> ( ( ( cls ` J ) ` S ) i^i T ) = (/) )