| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cncfrss | Structured version Visualization version GIF version | ||
| Description: Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| Ref | Expression |
|---|---|
| cncfrss | ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) |
| 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→𝐵) → 𝐴 ⊆ ℂ) |
| Colors of variables: wff setvar class |
| 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 |
| Copyright terms: Public domain | W3C validator |