Theorem cnf 15039

Description: A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)

Hypotheses

Ref	Expression
iscnp2.1	|- X = U. J
iscnp2.2	|- Y = U. K

Assertion

Ref	Expression
cnf	|- ( F e. ( J Cn K ) -> F : X --> Y )

Proof of Theorem cnf

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iscnp2.1	. . . 4 |- X = U. J
2		iscnp2.2	. . . 4 |- Y = U. K
3	1, 2	iscn2 15035	. . 3 |- ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : X --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
4	3	simprbi 275	. 2 |- ( F e. ( J Cn K ) -> ( F : X --> Y /\ A. x e. K ( `' F " x ) e. J ) )
5	4	simpld 112	1 |- ( F e. ( J Cn K ) -> F : X --> Y )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   e. wcel 2203   A.wral 2520   U.cuni 3907   `'ccnv 4739   "cima 4743   -->wf 5339  (class class class)co 6041   Topctop 14832   Cn ccn 15020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4221  ax-pow 4279  ax-pr 4314  ax-un 4545  ax-setind 4650

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2814  df-sbc 3042  df-csb 3138  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-pw 3667  df-sn 3688  df-pr 3689  df-op 3691  df-uni 3908  df-iun 3986  df-br 4103  df-opab 4165  df-mpt 4166  df-id 4405  df-xp 4746  df-rel 4747  df-cnv 4748  df-co 4749  df-dm 4750  df-rn 4751  df-res 4752  df-ima 4753  df-iota 5303  df-fun 5345  df-fn 5346  df-f 5347  df-fv 5351  df-ov 6044  df-oprab 6045  df-mpo 6046  df-1st 6325  df-2nd 6326  df-map 6875  df-top 14833  df-topon 14846  df-cn 15023

This theorem is referenced by:  cnco  15056  cnclima  15058  cnntri  15059  cnss1  15061  cnss2  15062  cncnpi  15063  cncnp2m  15066  cnrest  15070  cnrest2  15071  txcnmpt  15108  uptx  15109  txcn  15110  cnmpt11f  15119  cnmpt21f  15127  hmeocnv  15142  hmeores  15150  txhmeo  15154