Theorem iscn

Description: The predicate "the class F is a continuous function from topology J to topology K ". Definition of continuous function in Munkres p. 102. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Assertion	iscn	|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnfval	|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J Cn K ) = { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } )
2	1	eleq2d	|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> F e. { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } ) )
3		cnveq	|- ( f = F -> `' f = `' F )
4	3	imaeq1d	|- ( f = F -> ( `' f " y ) = ( `' F " y ) )
5	4	eleq1d	|- ( f = F -> ( ( `' f " y ) e. J <-> ( `' F " y ) e. J ) )
6	5	ralbidv	|- ( f = F -> ( A. y e. K ( `' f " y ) e. J <-> A. y e. K ( `' F " y ) e. J ) )
7	6	elrab	|- ( F e. { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } <-> ( F e. ( Y ^m X ) /\ A. y e. K ( `' F " y ) e. J ) )
8		toponmax	|- ( K e. ( TopOn ` Y ) -> Y e. K )
9		toponmax	|- ( J e. ( TopOn ` X ) -> X e. J )
10		elmapg	|- ( ( Y e. K /\ X e. J ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
11	8 9 10	syl2anr	|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
12	11	anbi1d	|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F e. ( Y ^m X ) /\ A. y e. K ( `' F " y ) e. J ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
13	7 12	syl5bb	|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
14	2 13	bitrd	|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )