Theorem cncfrss 24820

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 24807	. . 3 ⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑎 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑤))) < 𝑦)})
2	1	elmpocl1 7643	. 2 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ∈ 𝒫 ℂ)
3	2	elpwid 4582	1 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3050  ∃wrex 3059  {crab 3413   ⊆ wss 3924  𝒫 cpw 4573   class class class wbr 5116  ‘cfv 6527  (class class class)co 7399   ↑_m cmap 8834  ℂcc 11119   < clt 11261   − cmin 11458  ℝ⁺crp 13000  abscabs 15240  –cn→ccncf 24805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pr 5399

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-opab 5179  df-xp 5657  df-dm 5661  df-iota 6480  df-fv 6535  df-ov 7402  df-oprab 7403  df-mpo 7404  df-cncf 24807

This theorem is referenced by:  cncff  24822  cncfi  24823  rescncf  24826  cncfcdm  24827  cncfco  24836  cncfcompt2  24837  cncfmpt2f  24844  cncfcnvcn  24855  mulcncf  25383  cncombf  25596  cnlimci  25827  ulmcn  26345  efmul2picn  34549  mulcncff  45829  subcncff  45839  negcncfg  45840  addcncff  45843  ioccncflimc  45844  icocncflimc  45848  divcncff  45850