This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clsss

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

Ref Expression
Hypothesis clscld.1 
|- X = U. J
Assertion clsss 
|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( cls ` J ) ` T ) C_ ( ( cls ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 sstr2 
 |-  ( T C_ S -> ( S C_ x -> T C_ x ) )
3 2 adantr 
 |-  ( ( T C_ S /\ x e. ( Clsd ` J ) ) -> ( S C_ x -> T C_ x ) )
4 3 ss2rabdv 
 |-  ( T C_ S -> { x e. ( Clsd ` J ) | S C_ x } C_ { x e. ( Clsd ` J ) | T C_ x } )
5 intss 
 |-  ( { x e. ( Clsd ` J ) | S C_ x } C_ { x e. ( Clsd ` J ) | T C_ x } -> |^| { x e. ( Clsd ` J ) | T C_ x } C_ |^| { x e. ( Clsd ` J ) | S C_ x } )
6 4 5 syl 
 |-  ( T C_ S -> |^| { x e. ( Clsd ` J ) | T C_ x } C_ |^| { x e. ( Clsd ` J ) | S C_ x } )
7 6 3ad2ant3 
 |-  ( ( J e. Top /\ S C_ X /\ T C_ S ) -> |^| { x e. ( Clsd ` J ) | T C_ x } C_ |^| { x e. ( Clsd ` J ) | S C_ x } )
8 simp1 
 |-  ( ( J e. Top /\ S C_ X /\ T C_ S ) -> J e. Top )
9 sstr2 
 |-  ( T C_ S -> ( S C_ X -> T C_ X ) )
10 9 impcom 
 |-  ( ( S C_ X /\ T C_ S ) -> T C_ X )
11 10 3adant1 
 |-  ( ( J e. Top /\ S C_ X /\ T C_ S ) -> T C_ X )
12 1 clsval 
 |-  ( ( J e. Top /\ T C_ X ) -> ( ( cls ` J ) ` T ) = |^| { x e. ( Clsd ` J ) | T C_ x } )
13 8 11 12 syl2anc 
 |-  ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( cls ` J ) ` T ) = |^| { x e. ( Clsd ` J ) | T C_ x } )
14 1 clsval 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )
15 14 3adant3 
 |-  ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( cls ` J ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )
16 7 13 15 3sstr4d 
 |-  ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( cls ` J ) ` T ) C_ ( ( cls ` J ) ` S ) )