Theorem cntop1 22726

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062  ∪ cuni 4907  ^◡ccnv 5674   “ cima 5678  ⟶wf 6536  (class class class)co 7404  Topctop 22377   Cn ccn 22710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-map 8818  df-top 22378  df-topon 22395  df-cn 22713

This theorem is referenced by:  cnco  22752  cnclima  22754  cnntri  22757  cnclsi  22758  cnss2  22763  cncnpi  22764  cncnp2  22767  cnrest  22771  cnrest2  22772  cnrest2r  22773  lmcn  22791  cnt0  22832  cnt1  22836  cnhaus  22840  kgen2cn  23045  txcnmpt  23110  uptx  23111  txcn  23112  xkoco1cn  23143  xkoco2cn  23144  xkococnlem  23145  cnmpt21f  23158  qtopss  23201  qtopomap  23204  qtopcmap  23205  hmeofval  23244  hmeof1o  23250  hmeores  23257  hmphen  23271  txhmeo  23289  htpyco2  24477  hauseqcn  32816  cnmbfm  33200  hausgraph  41887  rfcnpre1  43636  fcnre  43642  cnneiima  47451