MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cntop2 Structured version   Visualization version   GIF version

Theorem cntop2 21835
Description: Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cntop2 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)

Proof of Theorem cntop2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqid 2824 . . . 4 𝐽 = 𝐽
2 eqid 2824 . . . 4 𝐾 = 𝐾
31, 2iscn2 21832 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹: 𝐽 𝐾 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
43simplbi 501 . 2 (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
54simprd 499 1 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2115  wral 3132   cuni 4819  ccnv 5535  cima 5539  wf 6332  (class class class)co 7138  Topctop 21487   Cn ccn 21818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-fv 6344  df-ov 7141  df-oprab 7142  df-mpo 7143  df-map 8391  df-top 21488  df-topon 21505  df-cn 21821
This theorem is referenced by:  cnco  21860  cncls2i  21864  cnntri  21865  cnss1  21870  cncnpi  21872  cncnp2  21875  cnrest  21879  cnrest2r  21881  paste  21888  cncmp  21986  rncmp  21990  cnconn  22016  connima  22019  conncn  22020  2ndcomap  22052  kgen2cn  22153  txcnmpt  22218  uptx  22219  lmcn2  22243  xkoco1cn  22251  xkoco2cn  22252  xkococnlem  22253  cnmpt11  22257  cnmpt11f  22258  cnmpt1t  22259  cnmpt12  22261  cnmpt21  22265  cnmpt2t  22267  cnmpt22  22268  cnmpt22f  22269  cnmptcom  22272  cnmpt2k  22282  qtopeu  22310  hmeofval  22352  hmeof1o  22358  hmeontr  22363  hmeores  22365  hmeoqtop  22369  hmphen  22379  reghmph  22387  nrmhmph  22388  txhmeo  22397  xpstopnlem1  22403  flfcntr  22637  cnmpopc  23522  ishtpy  23566  htpyco1  23572  htpyco2  23573  isphtpy  23575  phtpyco2  23584  isphtpc  23588  pcofval  23604  pcopt  23616  pcopt2  23617  pcorevlem  23620  pi1cof  23653  pi1coghm  23655  cnmbfm  31539  cnpconn  32495
  Copyright terms: Public domain W3C validator