Theorem cntop2 23224

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∀wral 3053  ∪ cuni 4838  ^◡ccnv 5617   “ cima 5621  ⟶wf 6481  (class class class)co 7356  Topctop 22876   Cn ccn 23207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-map 8765  df-top 22877  df-topon 22894  df-cn 23210

This theorem is referenced by:  cnco  23249  cncls2i  23253  cnntri  23254  cnss1  23259  cncnpi  23261  cncnp2  23264  cnrest  23268  cnrest2r  23270  paste  23277  cncmp  23375  rncmp  23379  cnconn  23405  connima  23408  conncn  23409  2ndcomap  23441  kgen2cn  23542  txcnmpt  23607  uptx  23608  lmcn2  23632  xkoco1cn  23640  xkoco2cn  23641  xkococnlem  23642  cnmpt11  23646  cnmpt11f  23647  cnmpt1t  23648  cnmpt12  23650  cnmpt21  23654  cnmpt2t  23656  cnmpt22  23657  cnmpt22f  23658  cnmptcom  23661  cnmpt2k  23671  qtopeu  23699  hmeofval  23741  hmeof1o  23747  hmeontr  23752  hmeores  23754  hmeoqtop  23758  hmphen  23768  reghmph  23776  nrmhmph  23777  txhmeo  23786  xpstopnlem1  23792  flfcntr  24026  cnmpopc  24913  ishtpy  24957  htpyco1  24963  htpyco2  24964  isphtpy  24966  phtpyco2  24975  isphtpc  24979  pcofval  24995  pcopt  25007  pcopt2  25008  pcorevlem  25011  pi1cof  25044  pi1coghm  25046  cnmbfm  34447  cnpconn  35458  cnneiima  49407