Theorem cntop2 23197

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052  ∪ cuni 4865  ^◡ccnv 5631   “ cima 5635  ⟶wf 6496  (class class class)co 7368  Topctop 22849   Cn ccn 23180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-map 8777  df-top 22850  df-topon 22867  df-cn 23183

This theorem is referenced by:  cnco  23222  cncls2i  23226  cnntri  23227  cnss1  23232  cncnpi  23234  cncnp2  23237  cnrest  23241  cnrest2r  23243  paste  23250  cncmp  23348  rncmp  23352  cnconn  23378  connima  23381  conncn  23382  2ndcomap  23414  kgen2cn  23515  txcnmpt  23580  uptx  23581  lmcn2  23605  xkoco1cn  23613  xkoco2cn  23614  xkococnlem  23615  cnmpt11  23619  cnmpt11f  23620  cnmpt1t  23621  cnmpt12  23623  cnmpt21  23627  cnmpt2t  23629  cnmpt22  23630  cnmpt22f  23631  cnmptcom  23634  cnmpt2k  23644  qtopeu  23672  hmeofval  23714  hmeof1o  23720  hmeontr  23725  hmeores  23727  hmeoqtop  23731  hmphen  23741  reghmph  23749  nrmhmph  23750  txhmeo  23759  xpstopnlem1  23765  flfcntr  23999  cnmpopc  24890  ishtpy  24939  htpyco1  24945  htpyco2  24946  isphtpy  24948  phtpyco2  24957  isphtpc  24961  pcofval  24978  pcopt  24990  pcopt2  24991  pcorevlem  24994  pi1cof  25027  pi1coghm  25029  cnmbfm  34441  cnpconn  35446  cnneiima  49276