Metamath Proof Explorer

Theorem lpss2

Description: Limit points of a subset are limit points of the larger set. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypothesis lpss2.1 
|- X = U. J
Assertion lpss2 
|- ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( limPt ` J ) ` B ) C_ ( ( limPt ` J ) ` A ) )

Proof

Step Hyp Ref Expression
1 lpss2.1 
 |-  X = U. J
2 1 lpss3 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( limPt ` J ) ` B ) C_ ( ( limPt ` J ) ` A ) )