# Metamath Proof Explorer

## Theorem cnima

Description: An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006)

Ref Expression
Assertion cnima ${⊢}\left({F}\in \left({J}\mathrm{Cn}{K}\right)\wedge {A}\in {K}\right)\to {{F}}^{-1}\left[{A}\right]\in {J}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\bigcup {J}=\bigcup {J}$
2 eqid ${⊢}\bigcup {K}=\bigcup {K}$
3 1 2 iscn2 ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)↔\left(\left({J}\in \mathrm{Top}\wedge {K}\in \mathrm{Top}\right)\wedge \left({F}:\bigcup {J}⟶\bigcup {K}\wedge \forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {J}\right)\right)$
4 3 simprbi ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to \left({F}:\bigcup {J}⟶\bigcup {K}\wedge \forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {J}\right)$
5 4 simprd ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to \forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {J}$
6 imaeq2 ${⊢}{x}={A}\to {{F}}^{-1}\left[{x}\right]={{F}}^{-1}\left[{A}\right]$
7 6 eleq1d ${⊢}{x}={A}\to \left({{F}}^{-1}\left[{x}\right]\in {J}↔{{F}}^{-1}\left[{A}\right]\in {J}\right)$
8 7 rspccva ${⊢}\left(\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {J}\wedge {A}\in {K}\right)\to {{F}}^{-1}\left[{A}\right]\in {J}$
9 5 8 sylan ${⊢}\left({F}\in \left({J}\mathrm{Cn}{K}\right)\wedge {A}\in {K}\right)\to {{F}}^{-1}\left[{A}\right]\in {J}$