# Metamath Proof Explorer

## Theorem kur14lem2

Description: Lemma for kur14 . Write interior in terms of closure and complement: i A = c k c A where c is complement and k is closure. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses kur14lem.j ${⊢}{J}\in \mathrm{Top}$
kur14lem.x ${⊢}{X}=\bigcup {J}$
kur14lem.k ${⊢}{K}=\mathrm{cls}\left({J}\right)$
kur14lem.i ${⊢}{I}=\mathrm{int}\left({J}\right)$
kur14lem.a ${⊢}{A}\subseteq {X}$
Assertion kur14lem2 ${⊢}{I}\left({A}\right)={X}\setminus {K}\left({X}\setminus {A}\right)$

### Proof

Step Hyp Ref Expression
1 kur14lem.j ${⊢}{J}\in \mathrm{Top}$
2 kur14lem.x ${⊢}{X}=\bigcup {J}$
3 kur14lem.k ${⊢}{K}=\mathrm{cls}\left({J}\right)$
4 kur14lem.i ${⊢}{I}=\mathrm{int}\left({J}\right)$
5 kur14lem.a ${⊢}{A}\subseteq {X}$
6 2 ntrval2 ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\subseteq {X}\right)\to \mathrm{int}\left({J}\right)\left({A}\right)={X}\setminus \mathrm{cls}\left({J}\right)\left({X}\setminus {A}\right)$
7 1 5 6 mp2an ${⊢}\mathrm{int}\left({J}\right)\left({A}\right)={X}\setminus \mathrm{cls}\left({J}\right)\left({X}\setminus {A}\right)$
8 4 fveq1i ${⊢}{I}\left({A}\right)=\mathrm{int}\left({J}\right)\left({A}\right)$
9 3 fveq1i ${⊢}{K}\left({X}\setminus {A}\right)=\mathrm{cls}\left({J}\right)\left({X}\setminus {A}\right)$
10 9 difeq2i ${⊢}{X}\setminus {K}\left({X}\setminus {A}\right)={X}\setminus \mathrm{cls}\left({J}\right)\left({X}\setminus {A}\right)$
11 7 8 10 3eqtr4i ${⊢}{I}\left({A}\right)={X}\setminus {K}\left({X}\setminus {A}\right)$