Theorem cntop1 21373

Description: Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
cntop1	⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)

Proof of Theorem cntop1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2799	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
2		eqid 2799	. . . 4 ⊢ ∪ 𝐾 = ∪ 𝐾
3	1, 2	iscn2 21371	. . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
4	3	simplbi 492	. 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
5	4	simpld 489	1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)

Syntax hints:   → wi 4   ∧ wa 385   ∈ wcel 2157  ∀wral 3089  ∪ cuni 4628  ^◡ccnv 5311   “ cima 5315  ⟶wf 6097  (class class class)co 6878  Topctop 21026   Cn ccn 21357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097  ax-un 7183

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109  df-ov 6881  df-oprab 6882  df-mpt2 6883  df-map 8097  df-top 21027  df-topon 21044  df-cn 21360

This theorem is referenced by:  cnco  21399  cnclima  21401  cnntri  21404  cnclsi  21405  cnss2  21410  cncnpi  21411  cncnp2  21414  cnrest  21418  cnrest2  21419  cnrest2r  21420  lmcn  21438  cnt0  21479  cnt1  21483  cnhaus  21487  kgen2cn  21691  txcnmpt  21756  uptx  21757  txcn  21758  xkoco1cn  21789  xkoco2cn  21790  xkococnlem  21791  cnmpt21f  21804  qtopss  21847  qtopomap  21850  qtopcmap  21851  hmeofval  21890  hmeof1o  21896  hmeores  21903  hmphen  21917  txhmeo  21935  htpyco2  23106  hauseqcn  30457  cnmbfm  30841  hausgraph  38575  rfcnpre1  39938  fcnre  39944