Theorem cntop2 21093

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 2651	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
2		eqid 2651	. . . 4 ⊢ ∪ 𝐾 = ∪ 𝐾
3	1, 2	iscn2 21090	. . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
4	3	simplbi 475	. 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
5	4	simprd 478	1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2030  ∀wral 2941  ∪ cuni 4468  ^◡ccnv 5142   “ cima 5146  ⟶wf 5922  (class class class)co 6690  Topctop 20746   Cn ccn 21076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-map 7901  df-top 20747  df-topon 20764  df-cn 21079

This theorem is referenced by:  cnco  21118  cncls2i  21122  cnntri  21123  cnss1  21128  cncnpi  21130  cncnp2  21133  cnrest  21137  cnrest2r  21139  paste  21146  cncmp  21243  rncmp  21247  cnconn  21273  connima  21276  conncn  21277  2ndcomap  21309  kgen2cn  21410  txcnmpt  21475  uptx  21476  lmcn2  21500  xkoco1cn  21508  xkoco2cn  21509  xkococnlem  21510  cnmpt11  21514  cnmpt11f  21515  cnmpt1t  21516  cnmpt12  21518  cnmpt21  21522  cnmpt2t  21524  cnmpt22  21525  cnmpt22f  21526  cnmptcom  21529  cnmpt2k  21539  qtopeu  21567  hmeofval  21609  hmeof1o  21615  hmeontr  21620  hmeores  21622  hmeoqtop  21626  hmphen  21636  reghmph  21644  nrmhmph  21645  txhmeo  21654  xpstopnlem1  21660  flfcntr  21894  cnmpt2pc  22774  ishtpy  22818  htpyco1  22824  htpyco2  22825  isphtpy  22827  phtpyco2  22836  isphtpc  22840  pcofval  22856  pcopt  22868  pcopt2  22869  pcorevlem  22872  pi1cof  22905  pi1coghm  22907  cnmbfm  30453  cnpconn  31338