Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fcnre Structured version   Visualization version   GIF version

Theorem fcnre 42269
Description: A function continuous with respect to the standard topology, is a real mapping. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
fcnre.1 𝐾 = (topGen‘ran (,))
fcnre.3 𝑇 = 𝐽
sfcnre.5 𝐶 = (𝐽 Cn 𝐾)
fcnre.6 (𝜑𝐹𝐶)
Assertion
Ref Expression
fcnre (𝜑𝐹:𝑇⟶ℝ)

Proof of Theorem fcnre
StepHypRef Expression
1 fcnre.6 . . . . 5 (𝜑𝐹𝐶)
2 sfcnre.5 . . . . 5 𝐶 = (𝐽 Cn 𝐾)
31, 2eleqtrdi 2849 . . . 4 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
4 cntop1 22161 . . . 4 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
53, 4syl 17 . . 3 (𝜑𝐽 ∈ Top)
6 fcnre.3 . . . 4 𝑇 = 𝐽
76toptopon 21838 . . 3 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑇))
85, 7sylib 221 . 2 (𝜑𝐽 ∈ (TopOn‘𝑇))
9 fcnre.1 . . . 4 𝐾 = (topGen‘ran (,))
10 retopon 23685 . . . 4 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
119, 10eqeltri 2835 . . 3 𝐾 ∈ (TopOn‘ℝ)
1211a1i 11 . 2 (𝜑𝐾 ∈ (TopOn‘ℝ))
13 cnf2 22170 . 2 ((𝐽 ∈ (TopOn‘𝑇) ∧ 𝐾 ∈ (TopOn‘ℝ) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑇⟶ℝ)
148, 12, 3, 13syl3anc 1373 1 (𝜑𝐹:𝑇⟶ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2111   cuni 4833  ran crn 5566  wf 6393  cfv 6397  (class class class)co 7231  cr 10752  (,)cioo 12959  topGenctg 16966  Topctop 21814  TopOnctopon 21831   Cn ccn 22145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-cnex 10809  ax-resscn 10810  ax-pre-lttri 10827  ax-pre-lttrn 10828
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-po 5482  df-so 5483  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-ov 7234  df-oprab 7235  df-mpo 7236  df-1st 7779  df-2nd 7780  df-er 8411  df-map 8530  df-en 8647  df-dom 8648  df-sdom 8649  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-ioo 12963  df-topgen 16972  df-top 21815  df-topon 21832  df-bases 21867  df-cn 22148
This theorem is referenced by:  rfcnpre2  42275  cncmpmax  42276  rfcnpre3  42277  rfcnpre4  42278  rfcnnnub  42280  stoweidlem28  43272  stoweidlem29  43273  stoweidlem36  43280  stoweidlem43  43287  stoweidlem44  43288  stoweidlem47  43291  stoweidlem52  43296  stoweidlem57  43301  stoweidlem59  43303  stoweidlem60  43304  stoweidlem61  43305  stoweidlem62  43306  stoweid  43307
  Copyright terms: Public domain W3C validator