Metamath Proof Explorer


Theorem kur14lem3

Description: Lemma for kur14 . A closure is a subset of the base set. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses kur14lem.j
|- J e. Top
kur14lem.x
|- X = U. J
kur14lem.k
|- K = ( cls ` J )
kur14lem.i
|- I = ( int ` J )
kur14lem.a
|- A C_ X
Assertion kur14lem3
|- ( K ` A ) C_ X

Proof

Step Hyp Ref Expression
1 kur14lem.j
 |-  J e. Top
2 kur14lem.x
 |-  X = U. J
3 kur14lem.k
 |-  K = ( cls ` J )
4 kur14lem.i
 |-  I = ( int ` J )
5 kur14lem.a
 |-  A C_ X
6 3 fveq1i
 |-  ( K ` A ) = ( ( cls ` J ) ` A )
7 2 clsss3
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` A ) C_ X )
8 1 5 7 mp2an
 |-  ( ( cls ` J ) ` A ) C_ X
9 6 8 eqsstri
 |-  ( K ` A ) C_ X