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

Theorem rfcnpre1 39696
 Description: If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than a given extended real B is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
rfcnpre1.1 𝑥𝐵
rfcnpre1.2 𝑥𝐹
rfcnpre1.3 𝑥𝜑
rfcnpre1.4 𝐾 = (topGen‘ran (,))
rfcnpre1.5 𝑋 = 𝐽
rfcnpre1.6 𝐴 = {𝑥𝑋𝐵 < (𝐹𝑥)}
rfcnpre1.7 (𝜑𝐵 ∈ ℝ*)
rfcnpre1.8 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
Assertion
Ref Expression
rfcnpre1 (𝜑𝐴𝐽)

Proof of Theorem rfcnpre1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 rfcnpre1.3 . . . 4 𝑥𝜑
2 rfcnpre1.2 . . . . . 6 𝑥𝐹
32nfcnv 5457 . . . . 5 𝑥𝐹
4 rfcnpre1.1 . . . . . 6 𝑥𝐵
5 nfcv 2903 . . . . . 6 𝑥(,)
6 nfcv 2903 . . . . . 6 𝑥+∞
74, 5, 6nfov 6841 . . . . 5 𝑥(𝐵(,)+∞)
83, 7nfima 5633 . . . 4 𝑥(𝐹 “ (𝐵(,)+∞))
9 nfrab1 3262 . . . 4 𝑥{𝑥𝑋𝐵 < (𝐹𝑥)}
10 rfcnpre1.8 . . . . . . . . . 10 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
11 cntop1 21267 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
1210, 11syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ Top)
13 rfcnpre1.5 . . . . . . . . . . . 12 𝑋 = 𝐽
14 istopon 20940 . . . . . . . . . . . 12 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
1512, 13, 14sylanblrc 700 . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
16 rfcnpre1.4 . . . . . . . . . . . 12 𝐾 = (topGen‘ran (,))
17 retopon 22789 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
1816, 17eqeltri 2836 . . . . . . . . . . 11 𝐾 ∈ (TopOn‘ℝ)
19 iscn 21262 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘ℝ)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶ℝ ∧ ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽)))
2015, 18, 19sylancl 697 . . . . . . . . . 10 (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶ℝ ∧ ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽)))
2110, 20mpbid 222 . . . . . . . . 9 (𝜑 → (𝐹:𝑋⟶ℝ ∧ ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽))
2221simpld 477 . . . . . . . 8 (𝜑𝐹:𝑋⟶ℝ)
2322ffvelrnda 6524 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ ℝ)
24 rfcnpre1.7 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ*)
25 elioopnf 12481 . . . . . . . . 9 (𝐵 ∈ ℝ* → ((𝐹𝑥) ∈ (𝐵(,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 𝐵 < (𝐹𝑥))))
2624, 25syl 17 . . . . . . . 8 (𝜑 → ((𝐹𝑥) ∈ (𝐵(,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 𝐵 < (𝐹𝑥))))
2726baibd 986 . . . . . . 7 ((𝜑 ∧ (𝐹𝑥) ∈ ℝ) → ((𝐹𝑥) ∈ (𝐵(,)+∞) ↔ 𝐵 < (𝐹𝑥)))
2823, 27syldan 488 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∈ (𝐵(,)+∞) ↔ 𝐵 < (𝐹𝑥)))
2928pm5.32da 676 . . . . 5 (𝜑 → ((𝑥𝑋 ∧ (𝐹𝑥) ∈ (𝐵(,)+∞)) ↔ (𝑥𝑋𝐵 < (𝐹𝑥))))
30 ffn 6207 . . . . . 6 (𝐹:𝑋⟶ℝ → 𝐹 Fn 𝑋)
31 elpreima 6502 . . . . . 6 (𝐹 Fn 𝑋 → (𝑥 ∈ (𝐹 “ (𝐵(,)+∞)) ↔ (𝑥𝑋 ∧ (𝐹𝑥) ∈ (𝐵(,)+∞))))
3222, 30, 313syl 18 . . . . 5 (𝜑 → (𝑥 ∈ (𝐹 “ (𝐵(,)+∞)) ↔ (𝑥𝑋 ∧ (𝐹𝑥) ∈ (𝐵(,)+∞))))
33 rabid 3255 . . . . . 6 (𝑥 ∈ {𝑥𝑋𝐵 < (𝐹𝑥)} ↔ (𝑥𝑋𝐵 < (𝐹𝑥)))
3433a1i 11 . . . . 5 (𝜑 → (𝑥 ∈ {𝑥𝑋𝐵 < (𝐹𝑥)} ↔ (𝑥𝑋𝐵 < (𝐹𝑥))))
3529, 32, 343bitr4d 300 . . . 4 (𝜑 → (𝑥 ∈ (𝐹 “ (𝐵(,)+∞)) ↔ 𝑥 ∈ {𝑥𝑋𝐵 < (𝐹𝑥)}))
361, 8, 9, 35eqrd 3764 . . 3 (𝜑 → (𝐹 “ (𝐵(,)+∞)) = {𝑥𝑋𝐵 < (𝐹𝑥)})
37 rfcnpre1.6 . . 3 𝐴 = {𝑥𝑋𝐵 < (𝐹𝑥)}
3836, 37syl6eqr 2813 . 2 (𝜑 → (𝐹 “ (𝐵(,)+∞)) = 𝐴)
39 iooretop 22791 . . . 4 (𝐵(,)+∞) ∈ (topGen‘ran (,))
4039, 16eleqtrri 2839 . . 3 (𝐵(,)+∞) ∈ 𝐾
41 cnima 21292 . . 3 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐵(,)+∞) ∈ 𝐾) → (𝐹 “ (𝐵(,)+∞)) ∈ 𝐽)
4210, 40, 41sylancl 697 . 2 (𝜑 → (𝐹 “ (𝐵(,)+∞)) ∈ 𝐽)
4338, 42eqeltrrd 2841 1 (𝜑𝐴𝐽)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632  Ⅎwnf 1857   ∈ wcel 2140  Ⅎwnfc 2890  ∀wral 3051  {crab 3055  ∪ cuni 4589   class class class wbr 4805  ◡ccnv 5266  ran crn 5268   “ cima 5270   Fn wfn 6045  ⟶wf 6046  ‘cfv 6050  (class class class)co 6815  ℝcr 10148  +∞cpnf 10284  ℝ*cxr 10286   < clt 10287  (,)cioo 12389  topGenctg 16321  Topctop 20921  TopOnctopon 20938   Cn ccn 21251 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-cnex 10205  ax-resscn 10206  ax-1cn 10207  ax-icn 10208  ax-addcl 10209  ax-addrcl 10210  ax-mulcl 10211  ax-mulrcl 10212  ax-mulcom 10213  ax-addass 10214  ax-mulass 10215  ax-distr 10216  ax-i2m1 10217  ax-1ne0 10218  ax-1rid 10219  ax-rnegex 10220  ax-rrecex 10221  ax-cnre 10222  ax-pre-lttri 10223  ax-pre-lttrn 10224  ax-pre-ltadd 10225  ax-pre-mulgt0 10226  ax-pre-sup 10227 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-pred 5842  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-om 7233  df-1st 7335  df-2nd 7336  df-wrecs 7578  df-recs 7639  df-rdg 7677  df-er 7914  df-map 8028  df-en 8125  df-dom 8126  df-sdom 8127  df-sup 8516  df-inf 8517  df-pnf 10289  df-mnf 10290  df-xr 10291  df-ltxr 10292  df-le 10293  df-sub 10481  df-neg 10482  df-div 10898  df-nn 11234  df-n0 11506  df-z 11591  df-uz 11901  df-q 12003  df-ioo 12393  df-topgen 16327  df-top 20922  df-topon 20939  df-bases 20973  df-cn 21254 This theorem is referenced by:  stoweidlem46  40785
 Copyright terms: Public domain W3C validator