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

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