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

Theorem cntop2 21779
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 2821 . . . 4 𝐽 = 𝐽
2 eqid 2821 . . . 4 𝐾 = 𝐾
31, 2iscn2 21776 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹: 𝐽 𝐾 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
43simplbi 498 . 2 (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
54simprd 496 1 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wral 3138   cuni 4832  ccnv 5548  cima 5552  wf 6345  (class class class)co 7145  Topctop 21431   Cn ccn 21762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-ov 7148  df-oprab 7149  df-mpo 7150  df-map 8398  df-top 21432  df-topon 21449  df-cn 21765
This theorem is referenced by:  cnco  21804  cncls2i  21808  cnntri  21809  cnss1  21814  cncnpi  21816  cncnp2  21819  cnrest  21823  cnrest2r  21825  paste  21832  cncmp  21930  rncmp  21934  cnconn  21960  connima  21963  conncn  21964  2ndcomap  21996  kgen2cn  22097  txcnmpt  22162  uptx  22163  lmcn2  22187  xkoco1cn  22195  xkoco2cn  22196  xkococnlem  22197  cnmpt11  22201  cnmpt11f  22202  cnmpt1t  22203  cnmpt12  22205  cnmpt21  22209  cnmpt2t  22211  cnmpt22  22212  cnmpt22f  22213  cnmptcom  22216  cnmpt2k  22226  qtopeu  22254  hmeofval  22296  hmeof1o  22302  hmeontr  22307  hmeores  22309  hmeoqtop  22313  hmphen  22323  reghmph  22331  nrmhmph  22332  txhmeo  22341  xpstopnlem1  22347  flfcntr  22581  cnmpopc  23461  ishtpy  23505  htpyco1  23511  htpyco2  23512  isphtpy  23514  phtpyco2  23523  isphtpc  23527  pcofval  23543  pcopt  23555  pcopt2  23556  pcorevlem  23559  pi1cof  23592  pi1coghm  23594  cnmbfm  31421  cnpconn  32375
  Copyright terms: Public domain W3C validator