ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  limcrcl Unicode version

Theorem limcrcl 13123
Description: Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
Assertion
Ref Expression
limcrcl  |-  ( C  e.  ( F lim CC  B )  ->  ( F : dom  F --> CC  /\  dom  F  C_  CC  /\  B  e.  CC ) )

Proof of Theorem limcrcl
Dummy variables  d  e  f  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-limced 13121 . . 3  |- lim CC  =  ( f  e.  ( CC  ^pm  CC ) ,  x  e.  CC  |->  { y  e.  CC  |  ( ( f : dom  f --> CC 
/\  dom  f  C_  CC )  /\  (
x  e.  CC  /\  A. e  e.  RR+  E. d  e.  RR+  A. z  e. 
dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e ) ) ) } )
21elmpocl 6021 . 2  |-  ( C  e.  ( F lim CC  B )  ->  ( F  e.  ( CC  ^pm 
CC )  /\  B  e.  CC ) )
3 cnex 7859 . . . . 5  |-  CC  e.  _V
43, 3elpm2 6628 . . . 4  |-  ( F  e.  ( CC  ^pm  CC )  <->  ( F : dom  F --> CC  /\  dom  F 
C_  CC ) )
54anbi1i 454 . . 3  |-  ( ( F  e.  ( CC 
^pm  CC )  /\  B  e.  CC )  <->  ( ( F : dom  F --> CC  /\  dom  F  C_  CC )  /\  B  e.  CC ) )
6 df-3an 965 . . 3  |-  ( ( F : dom  F --> CC  /\  dom  F  C_  CC  /\  B  e.  CC ) 
<->  ( ( F : dom  F --> CC  /\  dom  F 
C_  CC )  /\  B  e.  CC )
)
75, 6bitr4i 186 . 2  |-  ( ( F  e.  ( CC 
^pm  CC )  /\  B  e.  CC )  <->  ( F : dom  F --> CC  /\  dom  F  C_  CC  /\  B  e.  CC ) )
82, 7sylib 121 1  |-  ( C  e.  ( F lim CC  B )  ->  ( F : dom  F --> CC  /\  dom  F  C_  CC  /\  B  e.  CC ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 963    e. wcel 2128   A.wral 2435   E.wrex 2436   {crab 2439    C_ wss 3102   class class class wbr 3967   dom cdm 4589   -->wf 5169   ` cfv 5173  (class class class)co 5827    ^pm cpm 6597   CCcc 7733    < clt 7915    - cmin 8051   # cap 8461   RR+crp 9567   abscabs 10909   lim CC climc 13119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4085  ax-pow 4138  ax-pr 4172  ax-un 4396  ax-setind 4499  ax-cnex 7826
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-br 3968  df-opab 4029  df-id 4256  df-xp 4595  df-rel 4596  df-cnv 4597  df-co 4598  df-dm 4599  df-rn 4600  df-iota 5138  df-fun 5175  df-fn 5176  df-f 5177  df-fv 5181  df-ov 5830  df-oprab 5831  df-mpo 5832  df-pm 6599  df-limced 13121
This theorem is referenced by:  limccl  13124  limcdifap  13127  limcimolemlt  13129  limcresi  13131  limccnpcntop  13140  limccnp2lem  13141  limccnp2cntop  13142  limccoap  13143
  Copyright terms: Public domain W3C validator