Metamath Proof Explorer


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