Theorem cntop2 21416

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.

Step	Hyp	Ref	Expression
1		eqid 2825	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
2		eqid 2825	. . . 4 ⊢ ∪ 𝐾 = ∪ 𝐾
3	1, 2	iscn2 21413	. . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
4	3	simplbi 493	. 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
5	4	simprd 491	1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2166  ∀wral 3117  ∪ cuni 4658  ^◡ccnv 5341   “ cima 5345  ⟶wf 6119  (class class class)co 6905  Topctop 21068   Cn ccn 21399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-map 8124  df-top 21069  df-topon 21086  df-cn 21402

This theorem is referenced by:  cnco  21441  cncls2i  21445  cnntri  21446  cnss1  21451  cncnpi  21453  cncnp2  21456  cnrest  21460  cnrest2r  21462  paste  21469  cncmp  21566  rncmp  21570  cnconn  21596  connima  21599  conncn  21600  2ndcomap  21632  kgen2cn  21733  txcnmpt  21798  uptx  21799  lmcn2  21823  xkoco1cn  21831  xkoco2cn  21832  xkococnlem  21833  cnmpt11  21837  cnmpt11f  21838  cnmpt1t  21839  cnmpt12  21841  cnmpt21  21845  cnmpt2t  21847  cnmpt22  21848  cnmpt22f  21849  cnmptcom  21852  cnmpt2k  21862  qtopeu  21890  hmeofval  21932  hmeof1o  21938  hmeontr  21943  hmeores  21945  hmeoqtop  21949  hmphen  21959  reghmph  21967  nrmhmph  21968  txhmeo  21977  xpstopnlem1  21983  flfcntr  22217  cnmpt2pc  23097  ishtpy  23141  htpyco1  23147  htpyco2  23148  isphtpy  23150  phtpyco2  23159  isphtpc  23163  pcofval  23179  pcopt  23191  pcopt2  23192  pcorevlem  23195  pi1cof  23228  pi1coghm  23230  cnmbfm  30870  cnpconn  31758