Metamath Proof Explorer


Theorem restclsseplem

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

Ref Expression
Hypotheses restcls2.1 φ J Top
restcls2.2 φ X = J
restcls2.3 φ Y X
restcls2.4 φ K = J 𝑡 Y
restcls2.5 φ S Clsd K
restclsseplem.6 φ S T =
restclsseplem.7 φ T Y
Assertion restclsseplem φ cls J S T =

Proof

Step Hyp Ref Expression
1 restcls2.1 φ J Top
2 restcls2.2 φ X = J
3 restcls2.3 φ Y X
4 restcls2.4 φ K = J 𝑡 Y
5 restcls2.5 φ S Clsd K
6 restclsseplem.6 φ S T =
7 restclsseplem.7 φ T Y
8 1 2 3 4 5 restcls2 φ S = cls J S Y
9 8 ineq1d φ S T = cls J S Y T
10 inass cls J S Y T = cls J S Y T
11 9 10 eqtrdi φ S T = cls J S Y T
12 sseqin2 T Y Y T = T
13 7 12 sylib φ Y T = T
14 13 ineq2d φ cls J S Y T = cls J S T
15 11 6 14 3eqtr3rd φ cls J S T =