Metamath Proof Explorer


Theorem kur14lem5

Description: Lemma for kur14 . Closure is an idempotent operation in the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses kur14lem.j J Top
kur14lem.x X = J
kur14lem.k K = cls J
kur14lem.i I = int J
kur14lem.a A X
Assertion kur14lem5 K K A = K A

Proof

Step Hyp Ref Expression
1 kur14lem.j J Top
2 kur14lem.x X = J
3 kur14lem.k K = cls J
4 kur14lem.i I = int J
5 kur14lem.a A X
6 2 clsidm J Top A X cls J cls J A = cls J A
7 1 5 6 mp2an cls J cls J A = cls J A
8 3 fveq1i K A = cls J A
9 3 8 fveq12i K K A = cls J cls J A
10 7 9 8 3eqtr4i K K A = K A