Theorem lpss3

Description: Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypothesis	lpfval.1	|- X = U. J
Assertion	lpss3	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( limPt ` J ) ` T ) C_ ( ( limPt ` J ) ` S ) )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	|- X = U. J
2		simp1	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> J e. Top )
3		simp2	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> S C_ X )
4	3	ssdifssd	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( S \ { x } ) C_ X )
5		simp3	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> T C_ S )
6	5	ssdifd	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( T \ { x } ) C_ ( S \ { x } ) )
7	1	clsss	|- ( ( J e. Top /\ ( S \ { x } ) C_ X /\ ( T \ { x } ) C_ ( S \ { x } ) ) -> ( ( cls ` J ) ` ( T \ { x } ) ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) )
8	2 4 6 7	syl3anc	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( cls ` J ) ` ( T \ { x } ) ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) )
9	8	sseld	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( x e. ( ( cls ` J ) ` ( T \ { x } ) ) -> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
10	5 3	sstrd	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> T C_ X )
11	1	islp	|- ( ( J e. Top /\ T C_ X ) -> ( x e. ( ( limPt ` J ) ` T ) <-> x e. ( ( cls ` J ) ` ( T \ { x } ) ) ) )
12	2 10 11	syl2anc	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( x e. ( ( limPt ` J ) ` T ) <-> x e. ( ( cls ` J ) ` ( T \ { x } ) ) ) )
13	1	islp	|- ( ( J e. Top /\ S C_ X ) -> ( x e. ( ( limPt ` J ) ` S ) <-> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
14	2 3 13	syl2anc	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( x e. ( ( limPt ` J ) ` S ) <-> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
15	9 12 14	3imtr4d	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( x e. ( ( limPt ` J ) ` T ) -> x e. ( ( limPt ` J ) ` S ) ) )
16	15	ssrdv	|- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( limPt ` J ) ` T ) C_ ( ( limPt ` J ) ` S ) )