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 )