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