This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( F e. ( J Cn K ) /\ A e. K ) -> ( `' F " A ) e. J )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 eqid 
 |-  U. K = U. K
3 1 2 iscn2 
 |-  ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : U. J --> U. K /\ A. x e. K ( `' F " x ) e. J ) ) )
4 3 simprbi 
 |-  ( F e. ( J Cn K ) -> ( F : U. J --> U. K /\ A. x e. K ( `' F " x ) e. J ) )
5 4 simprd 
 |-  ( F e. ( J Cn K ) -> A. x e. K ( `' F " x ) e. J )
6 imaeq2 
 |-  ( x = A -> ( `' F " x ) = ( `' F " A ) )
7 6 eleq1d 
 |-  ( x = A -> ( ( `' F " x ) e. J <-> ( `' F " A ) e. J ) )
8 7 rspccva 
 |-  ( ( A. x e. K ( `' F " x ) e. J /\ A e. K ) -> ( `' F " A ) e. J )
9 5 8 sylan 
 |-  ( ( F e. ( J Cn K ) /\ A e. K ) -> ( `' F " A ) e. J )