Theorem cncfrss 25007

Description: Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)

Assertion

Ref	Expression
cncfrss	⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)

Proof of Theorem cncfrss

Dummy variables 𝑎 𝑏 𝑓 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-cncf 24994	. . 3 ⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑎 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑤))) < 𝑦)})
2	1	elmpocl1 7642	. 2 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ∈ 𝒫 ℂ)
3	2	elpwid 4567	1 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089  {crab 3417   ⊆ wss 3907  𝒫 cpw 4558   class class class wbr 5104  ‘cfv 6525  (class class class)co 7400   ↑_m cmap 8812  ℂcc 11086   < clt 11231   − cmin 11429  ℝ⁺crp 13004  abscabs 15273  –cn→ccncf 24992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-xp 5657  df-dm 5661  df-iota 6481  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-cncf 24994

This theorem is referenced by:  cncff  25009  cncfi  25010  rescncf  25013  cncfcdm  25014  cncfco  25023  cncfcompt2  25024  cncfmpt2f  25031  cncfcnvcn  25041  mulcncf  25562  cncombf  25774  cnlimci  26005  ulmcn  26516  efmul2picn  34895  mulcncff  46443  subcncff  46453  negcncfg  46454  addcncff  46457  ioccncflimc  46458  icocncflimc  46462  divcncff  46464