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 ) )