MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cncnp Structured version   Unicode version

Theorem cncnp 20283
Description: A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cncnp  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  ->  ( F  e.  ( J  Cn  K
)  <->  ( F : X
--> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) ) )
Distinct variable groups:    x, F    x, J    x, K    x, X    x, Y

Proof of Theorem cncnp
Dummy variables  u  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iscn 20238 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  ->  ( F  e.  ( J  Cn  K
)  <->  ( F : X
--> Y  /\  A. y  e.  K  ( `' F " y )  e.  J ) ) )
21simprbda 627 . . 3  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  F : X --> Y )
3 eqid 2422 . . . . . . 7  |-  U. J  =  U. J
43cncnpi 20281 . . . . . 6  |-  ( ( F  e.  ( J  Cn  K )  /\  x  e.  U. J )  ->  F  e.  ( ( J  CnP  K
) `  x )
)
54ralrimiva 2839 . . . . 5  |-  ( F  e.  ( J  Cn  K )  ->  A. x  e.  U. J F  e.  ( ( J  CnP  K ) `  x ) )
65adantl 467 . . . 4  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  A. x  e.  U. J F  e.  ( ( J  CnP  K ) `  x ) )
7 toponuni 19929 . . . . . 6  |-  ( J  e.  (TopOn `  X
)  ->  X  =  U. J )
87ad2antrr 730 . . . . 5  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  X  =  U. J )
98raleqdv 3031 . . . 4  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  ( A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x )  <->  A. x  e.  U. J F  e.  ( ( J  CnP  K ) `  x ) ) )
106, 9mpbird 235 . . 3  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) )
112, 10jca 534 . 2  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) )
12 simprl 762 . . 3  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) )  ->  F : X --> Y )
13 cnvimass 5204 . . . . . . . . . 10  |-  ( `' F " y ) 
C_  dom  F
14 fdm 5747 . . . . . . . . . . 11  |-  ( F : X --> Y  ->  dom  F  =  X )
1514adantl 467 . . . . . . . . . 10  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K )  /\  F : X --> Y )  ->  dom  F  =  X )
1613, 15syl5sseq 3512 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K )  /\  F : X --> Y )  ->  ( `' F " y )  C_  X
)
17 ssralv 3525 . . . . . . . . 9  |-  ( ( `' F " y ) 
C_  X  ->  ( A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x )  ->  A. x  e.  ( `' F "
y ) F  e.  ( ( J  CnP  K ) `  x ) ) )
1816, 17syl 17 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K )  /\  F : X --> Y )  ->  ( A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x )  ->  A. x  e.  ( `' F " y ) F  e.  ( ( J  CnP  K ) `
 x ) ) )
19 simprr 764 . . . . . . . . . . . 12  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  (
x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  F  e.  ( ( J  CnP  K ) `  x ) )
20 simpllr 767 . . . . . . . . . . . 12  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  (
x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  y  e.  K )
21 ffn 5743 . . . . . . . . . . . . . 14  |-  ( F : X --> Y  ->  F  Fn  X )
2221ad2antlr 731 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  (
x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  F  Fn  X )
23 simprl 762 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  (
x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  x  e.  ( `' F "
y ) )
24 elpreima 6014 . . . . . . . . . . . . . 14  |-  ( F  Fn  X  ->  (
x  e.  ( `' F " y )  <-> 
( x  e.  X  /\  ( F `  x
)  e.  y ) ) )
2524simplbda 628 . . . . . . . . . . . . 13  |-  ( ( F  Fn  X  /\  x  e.  ( `' F " y ) )  ->  ( F `  x )  e.  y )
2622, 23, 25syl2anc 665 . . . . . . . . . . . 12  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  (
x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  ( F `  x )  e.  y )
27 cnpimaex 20259 . . . . . . . . . . . 12  |-  ( ( F  e.  ( ( J  CnP  K ) `
 x )  /\  y  e.  K  /\  ( F `  x )  e.  y )  ->  E. u  e.  J  ( x  e.  u  /\  ( F " u
)  C_  y )
)
2819, 20, 26, 27syl3anc 1264 . . . . . . . . . . 11  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  (
x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  E. u  e.  J  ( x  e.  u  /\  ( F " u )  C_  y ) )
29 simpllr 767 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  y  e.  K )  /\  F : X --> Y )  /\  ( x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  /\  u  e.  J )  ->  F : X --> Y )
30 ffun 5745 . . . . . . . . . . . . . . 15  |-  ( F : X --> Y  ->  Fun  F )
3129, 30syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  y  e.  K )  /\  F : X --> Y )  /\  ( x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  /\  u  e.  J )  ->  Fun  F )
32 simp-4l 774 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  (
x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  J  e.  (TopOn `  X )
)
33 toponss 19931 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  (TopOn `  X )  /\  u  e.  J )  ->  u  C_  X )
3432, 33sylan 473 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  y  e.  K )  /\  F : X --> Y )  /\  ( x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  /\  u  e.  J )  ->  u  C_  X )
3529, 14syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  y  e.  K )  /\  F : X --> Y )  /\  ( x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  /\  u  e.  J )  ->  dom  F  =  X )
3634, 35sseqtr4d 3501 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  y  e.  K )  /\  F : X --> Y )  /\  ( x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  /\  u  e.  J )  ->  u  C_ 
dom  F )
37 funimass3 6010 . . . . . . . . . . . . . 14  |-  ( ( Fun  F  /\  u  C_ 
dom  F )  -> 
( ( F "
u )  C_  y  <->  u 
C_  ( `' F " y ) ) )
3831, 36, 37syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  y  e.  K )  /\  F : X --> Y )  /\  ( x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  /\  u  e.  J )  ->  (
( F " u
)  C_  y  <->  u  C_  ( `' F " y ) ) )
3938anbi2d 708 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  y  e.  K )  /\  F : X --> Y )  /\  ( x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  /\  u  e.  J )  ->  (
( x  e.  u  /\  ( F " u
)  C_  y )  <->  ( x  e.  u  /\  u  C_  ( `' F " y ) ) ) )
4039rexbidva 2936 . . . . . . . . . . 11  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  (
x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  ( E. u  e.  J  ( x  e.  u  /\  ( F " u
)  C_  y )  <->  E. u  e.  J  ( x  e.  u  /\  u  C_  ( `' F " y ) ) ) )
4128, 40mpbid 213 . . . . . . . . . 10  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  (
x  e.  ( `' F " y )  /\  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  E. u  e.  J  ( x  e.  u  /\  u  C_  ( `' F "
y ) ) )
4241expr 618 . . . . . . . . 9  |-  ( ( ( ( ( J  e.  (TopOn `  X
)  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K
)  /\  F : X
--> Y )  /\  x  e.  ( `' F "
y ) )  -> 
( F  e.  ( ( J  CnP  K
) `  x )  ->  E. u  e.  J  ( x  e.  u  /\  u  C_  ( `' F " y ) ) ) )
4342ralimdva 2833 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K )  /\  F : X --> Y )  ->  ( A. x  e.  ( `' F "
y ) F  e.  ( ( J  CnP  K ) `  x )  ->  A. x  e.  ( `' F " y ) E. u  e.  J  ( x  e.  u  /\  u  C_  ( `' F " y ) ) ) )
4418, 43syld 45 . . . . . . 7  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K )  /\  F : X --> Y )  ->  ( A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x )  ->  A. x  e.  ( `' F " y ) E. u  e.  J  ( x  e.  u  /\  u  C_  ( `' F " y ) ) ) )
4544impr 623 . . . . . 6  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  y  e.  K )  /\  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K
) `  x )
) )  ->  A. x  e.  ( `' F "
y ) E. u  e.  J  ( x  e.  u  /\  u  C_  ( `' F "
y ) ) )
4645an32s 811 . . . . 5  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) )  /\  y  e.  K )  ->  A. x  e.  ( `' F "
y ) E. u  e.  J  ( x  e.  u  /\  u  C_  ( `' F "
y ) ) )
47 topontop 19928 . . . . . . 7  |-  ( J  e.  (TopOn `  X
)  ->  J  e.  Top )
4847ad3antrrr 734 . . . . . 6  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) )  /\  y  e.  K )  ->  J  e.  Top )
49 eltop2 19978 . . . . . 6  |-  ( J  e.  Top  ->  (
( `' F "
y )  e.  J  <->  A. x  e.  ( `' F " y ) E. u  e.  J  ( x  e.  u  /\  u  C_  ( `' F " y ) ) ) )
5048, 49syl 17 . . . . 5  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) )  /\  y  e.  K )  ->  (
( `' F "
y )  e.  J  <->  A. x  e.  ( `' F " y ) E. u  e.  J  ( x  e.  u  /\  u  C_  ( `' F " y ) ) ) )
5146, 50mpbird 235 . . . 4  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y ) )  /\  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) )  /\  y  e.  K )  ->  ( `' F " y )  e.  J )
5251ralrimiva 2839 . . 3  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) )  ->  A. y  e.  K  ( `' F " y )  e.  J )
531adantr 466 . . 3  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) )  ->  ( F  e.  ( J  Cn  K )  <->  ( F : X --> Y  /\  A. y  e.  K  ( `' F " y )  e.  J ) ) )
5412, 52, 53mpbir2and 930 . 2  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  ( F : X --> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) )  ->  F  e.  ( J  Cn  K
) )
5511, 54impbida 840 1  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  ->  ( F  e.  ( J  Cn  K
)  <->  ( F : X
--> Y  /\  A. x  e.  X  F  e.  ( ( J  CnP  K ) `  x ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1868   A.wral 2775   E.wrex 2776    C_ wss 3436   U.cuni 4216   `'ccnv 4849   dom cdm 4850   "cima 4853   Fun wfun 5592    Fn wfn 5593   -->wf 5594   ` cfv 5598  (class class class)co 6302   Topctop 19904  TopOnctopon 19905    Cn ccn 20227    CnP ccnp 20228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-fv 5606  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-1st 6804  df-2nd 6805  df-map 7479  df-topgen 15330  df-top 19908  df-topon 19910  df-cn 20230  df-cnp 20231
This theorem is referenced by:  cncnp2  20284  cnnei  20285  cnconst2  20286  1stccn  20465  ptcn  20629  cnflf  21004  cnfcf  21044  symgtgp  21103  ghmcnp  21116  metcn  21545  txmetcn  21550  cnlimc  22830  dvcn  22862  dvcnvre  22958  psercn  23368  abelth  23383  cxpcn3  23675  cvmlift2lem11  30032  cvmlift2lem12  30033  cvmlift3lem8  30045  ioccncflimc  37583  cncfuni  37584  icccncfext  37585  icocncflimc  37587  cncfiooicclem1  37591  dirkercncflem2  37786  dirkercncflem4  37788  dirkercncf  37789  fourierdlem32  37822  fourierdlem33  37823  fourierdlem62  37852  fourierdlem93  37883  fourierdlem101  37891
  Copyright terms: Public domain W3C validator