Theorem cntop2 23104

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  ∪ cuni 4867  ^◡ccnv 5630   “ cima 5634  ⟶wf 6495  (class class class)co 7369  Topctop 22756   Cn ccn 23087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-map 8778  df-top 22757  df-topon 22774  df-cn 23090

This theorem is referenced by:  cnco  23129  cncls2i  23133  cnntri  23134  cnss1  23139  cncnpi  23141  cncnp2  23144  cnrest  23148  cnrest2r  23150  paste  23157  cncmp  23255  rncmp  23259  cnconn  23285  connima  23288  conncn  23289  2ndcomap  23321  kgen2cn  23422  txcnmpt  23487  uptx  23488  lmcn2  23512  xkoco1cn  23520  xkoco2cn  23521  xkococnlem  23522  cnmpt11  23526  cnmpt11f  23527  cnmpt1t  23528  cnmpt12  23530  cnmpt21  23534  cnmpt2t  23536  cnmpt22  23537  cnmpt22f  23538  cnmptcom  23541  cnmpt2k  23551  qtopeu  23579  hmeofval  23621  hmeof1o  23627  hmeontr  23632  hmeores  23634  hmeoqtop  23638  hmphen  23648  reghmph  23656  nrmhmph  23657  txhmeo  23666  xpstopnlem1  23672  flfcntr  23906  cnmpopc  24798  ishtpy  24847  htpyco1  24853  htpyco2  24854  isphtpy  24856  phtpyco2  24865  isphtpc  24869  pcofval  24886  pcopt  24898  pcopt2  24899  pcorevlem  24902  pi1cof  24935  pi1coghm  24937  cnmbfm  34227  cnpconn  35190  cnneiima  48878