MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnf2 Structured version   Unicode version

Theorem cnf2 20263
Description: A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cnf2  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )  /\  F  e.  ( J  Cn  K ) )  ->  F : X --> Y )

Proof of Theorem cnf2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 iscn 20249 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  ->  ( F  e.  ( J  Cn  K
)  <->  ( F : X
--> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) ) )
21simprbda 627 . 2  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  F : X --> Y )
323impa 1200 1  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )  /\  F  e.  ( J  Cn  K ) )  ->  F : X --> Y )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982    e. wcel 1872   A.wral 2771   `'ccnv 4852   "cima 4856   -->wf 5597   ` cfv 5601  (class class class)co 6305  TopOnctopon 19916    Cn ccn 20238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-map 7485  df-top 19919  df-topon 19921  df-cn 20241
This theorem is referenced by:  iscncl  20283  cncls2  20287  cncls  20288  cnntr  20289  cnrest2  20300  cnrest2r  20301  ptcn  20640  txdis1cn  20648  lmcn2  20662  cnmpt11  20676  cnmpt1t  20678  cnmpt12  20680  cnmpt21  20684  cnmpt2t  20686  cnmpt22  20687  cnmpt22f  20688  cnmptcom  20691  cnmptkp  20693  cnmptk1  20694  cnmpt1k  20695  cnmptkk  20696  cnmptk1p  20698  cnmptk2  20699  cnmpt2k  20701  qtopss  20728  qtopeu  20729  qtopomap  20731  qtopcmap  20732  hmeof1o2  20776  xpstopnlem1  20822  xkocnv  20827  xkohmeo  20828  qtophmeo  20830  cnmpt1plusg  21100  cnmpt2plusg  21101  tsmsmhm  21158  cnmpt1vsca  21206  cnmpt2vsca  21207  cnmpt1ds  21858  cnmpt2ds  21859  fsumcn  21900  cnmpt2pc  21954  htpyco1  22007  htpyco2  22008  phtpyco2  22019  pi1xfrf  22082  pi1xfr  22084  pi1xfrcnvlem  22085  pi1xfrcnv  22086  pi1cof  22088  pi1coghm  22090  cnmpt1ip  22216  cnmpt2ip  22217  txsconlem  29971  txscon  29972  cvmlift3lem6  30055  fcnre  37319  refsumcn  37324  refsum2cnlem1  37331  icccncfext  37705  itgsubsticclem  37792
  Copyright terms: Public domain W3C validator