Theorem cntop2 23249

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 23246	. . 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 2108  ∀wral 3061  ∪ cuni 4907  ^◡ccnv 5684   “ cima 5688  ⟶wf 6557  (class class class)co 7431  Topctop 22899   Cn ccn 23232

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868  df-top 22900  df-topon 22917  df-cn 23235

This theorem is referenced by:  cnco  23274  cncls2i  23278  cnntri  23279  cnss1  23284  cncnpi  23286  cncnp2  23289  cnrest  23293  cnrest2r  23295  paste  23302  cncmp  23400  rncmp  23404  cnconn  23430  connima  23433  conncn  23434  2ndcomap  23466  kgen2cn  23567  txcnmpt  23632  uptx  23633  lmcn2  23657  xkoco1cn  23665  xkoco2cn  23666  xkococnlem  23667  cnmpt11  23671  cnmpt11f  23672  cnmpt1t  23673  cnmpt12  23675  cnmpt21  23679  cnmpt2t  23681  cnmpt22  23682  cnmpt22f  23683  cnmptcom  23686  cnmpt2k  23696  qtopeu  23724  hmeofval  23766  hmeof1o  23772  hmeontr  23777  hmeores  23779  hmeoqtop  23783  hmphen  23793  reghmph  23801  nrmhmph  23802  txhmeo  23811  xpstopnlem1  23817  flfcntr  24051  cnmpopc  24955  ishtpy  25004  htpyco1  25010  htpyco2  25011  isphtpy  25013  phtpyco2  25022  isphtpc  25026  pcofval  25043  pcopt  25055  pcopt2  25056  pcorevlem  25059  pi1cof  25092  pi1coghm  25094  cnmbfm  34265  cnpconn  35235  cnneiima  48814