Metamath Proof Explorer


Theorem restclsseplem

Description: Lemma for restclssep . (Contributed by Zhi Wang, 2-Sep-2024)

Ref Expression
Hypotheses restcls2.1 φJTop
restcls2.2 φX=J
restcls2.3 φYX
restcls2.4 φK=J𝑡Y
restcls2.5 φSClsdK
restclsseplem.6 φST=
restclsseplem.7 φTY
Assertion restclsseplem φclsJST=

Proof

Step Hyp Ref Expression
1 restcls2.1 φJTop
2 restcls2.2 φX=J
3 restcls2.3 φYX
4 restcls2.4 φK=J𝑡Y
5 restcls2.5 φSClsdK
6 restclsseplem.6 φST=
7 restclsseplem.7 φTY
8 1 2 3 4 5 restcls2 φS=clsJSY
9 8 ineq1d φST=clsJSYT
10 inass clsJSYT=clsJSYT
11 9 10 eqtrdi φST=clsJSYT
12 sseqin2 TYYT=T
13 7 12 sylib φYT=T
14 13 ineq2d φclsJSYT=clsJST
15 11 6 14 3eqtr3rd φclsJST=