Metamath Proof Explorer


Theorem clsss

Description: Subset relationship for closure. (Contributed by NM, 10-Feb-2007)

Ref Expression
Hypothesis clscld.1 X=J
Assertion clsss JTopSXTSclsJTclsJS

Proof

Step Hyp Ref Expression
1 clscld.1 X=J
2 sstr2 TSSxTx
3 2 adantr TSxClsdJSxTx
4 3 ss2rabdv TSxClsdJ|SxxClsdJ|Tx
5 intss xClsdJ|SxxClsdJ|TxxClsdJ|TxxClsdJ|Sx
6 4 5 syl TSxClsdJ|TxxClsdJ|Sx
7 6 3ad2ant3 JTopSXTSxClsdJ|TxxClsdJ|Sx
8 simp1 JTopSXTSJTop
9 sstr2 TSSXTX
10 9 impcom SXTSTX
11 10 3adant1 JTopSXTSTX
12 1 clsval JTopTXclsJT=xClsdJ|Tx
13 8 11 12 syl2anc JTopSXTSclsJT=xClsdJ|Tx
14 1 clsval JTopSXclsJS=xClsdJ|Sx
15 14 3adant3 JTopSXTSclsJS=xClsdJ|Sx
16 7 13 15 3sstr4d JTopSXTSclsJTclsJS