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

Theorem cnrest2 17114
Description: Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cnrest2  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ( F  e.  ( J  Cn  K )  <->  F  e.  ( J  Cn  ( Kt  B ) ) ) )

Proof of Theorem cnrest2
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cntop1 17070 . . . 4  |-  ( F  e.  ( J  Cn  K )  ->  J  e.  Top )
21a1i 10 . . 3  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ( F  e.  ( J  Cn  K )  ->  J  e.  Top ) )
3 eqid 2358 . . . . . . . 8  |-  U. J  =  U. J
4 eqid 2358 . . . . . . . 8  |-  U. K  =  U. K
53, 4cnf 17076 . . . . . . 7  |-  ( F  e.  ( J  Cn  K )  ->  F : U. J --> U. K
)
6 ffn 5469 . . . . . . 7  |-  ( F : U. J --> U. K  ->  F  Fn  U. J
)
75, 6syl 15 . . . . . 6  |-  ( F  e.  ( J  Cn  K )  ->  F  Fn  U. J )
87a1i 10 . . . . 5  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ( F  e.  ( J  Cn  K )  ->  F  Fn  U. J ) )
9 simp2 956 . . . . 5  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ran  F 
C_  B )
108, 9jctird 528 . . . 4  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ( F  e.  ( J  Cn  K )  ->  ( F  Fn  U. J  /\  ran  F  C_  B )
) )
11 df-f 5338 . . . 4  |-  ( F : U. J --> B  <->  ( F  Fn  U. J  /\  ran  F 
C_  B ) )
1210, 11syl6ibr 218 . . 3  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ( F  e.  ( J  Cn  K )  ->  F : U. J --> B ) )
132, 12jcad 519 . 2  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ( F  e.  ( J  Cn  K )  ->  ( J  e.  Top  /\  F : U. J --> B ) ) )
14 cntop1 17070 . . . . 5  |-  ( F  e.  ( J  Cn  ( Kt  B ) )  ->  J  e.  Top )
1514adantl 452 . . . 4  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  F  e.  ( J  Cn  ( Kt  B ) ) )  ->  J  e.  Top )
163toptopon 16771 . . . . . 6  |-  ( J  e.  Top  <->  J  e.  (TopOn `  U. J ) )
1715, 16sylib 188 . . . . 5  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  F  e.  ( J  Cn  ( Kt  B ) ) )  ->  J  e.  (TopOn `  U. J ) )
18 resttopon 16992 . . . . . . 7  |-  ( ( K  e.  (TopOn `  Y )  /\  B  C_  Y )  ->  ( Kt  B )  e.  (TopOn `  B ) )
19183adant2 974 . . . . . 6  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ( Kt  B )  e.  (TopOn `  B ) )
2019adantr 451 . . . . 5  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  F  e.  ( J  Cn  ( Kt  B ) ) )  ->  ( Kt  B )  e.  (TopOn `  B
) )
21 simpr 447 . . . . 5  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  F  e.  ( J  Cn  ( Kt  B ) ) )  ->  F  e.  ( J  Cn  ( Kt  B ) ) )
22 cnf2 17079 . . . . 5  |-  ( ( J  e.  (TopOn `  U. J )  /\  ( Kt  B )  e.  (TopOn `  B )  /\  F  e.  ( J  Cn  ( Kt  B ) ) )  ->  F : U. J
--> B )
2317, 20, 21, 22syl3anc 1182 . . . 4  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  F  e.  ( J  Cn  ( Kt  B ) ) )  ->  F : U. J
--> B )
2415, 23jca 518 . . 3  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  F  e.  ( J  Cn  ( Kt  B ) ) )  ->  ( J  e. 
Top  /\  F : U. J --> B ) )
2524ex 423 . 2  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ( F  e.  ( J  Cn  ( Kt  B ) )  -> 
( J  e.  Top  /\  F : U. J --> B ) ) )
26 vex 2867 . . . . . . . . 9  |-  x  e. 
_V
2726inex1 4234 . . . . . . . 8  |-  ( x  i^i  B )  e. 
_V
2827a1i 10 . . . . . . 7  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  x  e.  K
)  ->  ( x  i^i  B )  e.  _V )
29 simpl1 958 . . . . . . . 8  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  K  e.  (TopOn `  Y ) )
30 simpl3 960 . . . . . . . . 9  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  B  C_  Y
)
31 toponmax 16766 . . . . . . . . . 10  |-  ( K  e.  (TopOn `  Y
)  ->  Y  e.  K )
3229, 31syl 15 . . . . . . . . 9  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  Y  e.  K )
33 ssexg 4239 . . . . . . . . 9  |-  ( ( B  C_  Y  /\  Y  e.  K )  ->  B  e.  _V )
3430, 32, 33syl2anc 642 . . . . . . . 8  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  B  e.  _V )
35 elrest 13425 . . . . . . . 8  |-  ( ( K  e.  (TopOn `  Y )  /\  B  e.  _V )  ->  (
y  e.  ( Kt  B )  <->  E. x  e.  K  y  =  ( x  i^i  B ) ) )
3629, 34, 35syl2anc 642 . . . . . . 7  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( y  e.  ( Kt  B )  <->  E. x  e.  K  y  =  ( x  i^i  B ) ) )
37 imaeq2 5087 . . . . . . . . 9  |-  ( y  =  ( x  i^i 
B )  ->  ( `' F " y )  =  ( `' F " ( x  i^i  B
) ) )
3837eleq1d 2424 . . . . . . . 8  |-  ( y  =  ( x  i^i 
B )  ->  (
( `' F "
y )  e.  J  <->  ( `' F " ( x  i^i  B ) )  e.  J ) )
3938adantl 452 . . . . . . 7  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  y  =  ( x  i^i  B ) )  ->  ( ( `' F " y )  e.  J  <->  ( `' F " ( x  i^i 
B ) )  e.  J ) )
4028, 36, 39ralxfr2d 4629 . . . . . 6  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( A. y  e.  ( Kt  B
) ( `' F " y )  e.  J  <->  A. x  e.  K  ( `' F " ( x  i^i  B ) )  e.  J ) )
41 simplrr 737 . . . . . . . . . 10  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  x  e.  K
)  ->  F : U. J --> B )
42 ffun 5471 . . . . . . . . . 10  |-  ( F : U. J --> B  ->  Fun  F )
43 inpreima 5732 . . . . . . . . . 10  |-  ( Fun 
F  ->  ( `' F " ( x  i^i 
B ) )  =  ( ( `' F " x )  i^i  ( `' F " B ) ) )
4441, 42, 433syl 18 . . . . . . . . 9  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  x  e.  K
)  ->  ( `' F " ( x  i^i 
B ) )  =  ( ( `' F " x )  i^i  ( `' F " B ) ) )
45 cnvimass 5112 . . . . . . . . . . . 12  |-  ( `' F " x ) 
C_  dom  F
46 cnvimarndm 5113 . . . . . . . . . . . 12  |-  ( `' F " ran  F
)  =  dom  F
4745, 46sseqtr4i 3287 . . . . . . . . . . 11  |-  ( `' F " x ) 
C_  ( `' F " ran  F )
48 simpll2 995 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  x  e.  K
)  ->  ran  F  C_  B )
49 imass2 5128 . . . . . . . . . . . 12  |-  ( ran 
F  C_  B  ->  ( `' F " ran  F
)  C_  ( `' F " B ) )
5048, 49syl 15 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  x  e.  K
)  ->  ( `' F " ran  F ) 
C_  ( `' F " B ) )
5147, 50syl5ss 3266 . . . . . . . . . 10  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  x  e.  K
)  ->  ( `' F " x )  C_  ( `' F " B ) )
52 df-ss 3242 . . . . . . . . . 10  |-  ( ( `' F " x ) 
C_  ( `' F " B )  <->  ( ( `' F " x )  i^i  ( `' F " B ) )  =  ( `' F "
x ) )
5351, 52sylib 188 . . . . . . . . 9  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  x  e.  K
)  ->  ( ( `' F " x )  i^i  ( `' F " B ) )  =  ( `' F "
x ) )
5444, 53eqtrd 2390 . . . . . . . 8  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  x  e.  K
)  ->  ( `' F " ( x  i^i 
B ) )  =  ( `' F "
x ) )
5554eleq1d 2424 . . . . . . 7  |-  ( ( ( ( K  e.  (TopOn `  Y )  /\  ran  F  C_  B  /\  B  C_  Y )  /\  ( J  e. 
Top  /\  F : U. J --> B ) )  /\  x  e.  K
)  ->  ( ( `' F " ( x  i^i  B ) )  e.  J  <->  ( `' F " x )  e.  J ) )
5655ralbidva 2635 . . . . . 6  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( A. x  e.  K  ( `' F " ( x  i^i  B ) )  e.  J  <->  A. x  e.  K  ( `' F " x )  e.  J ) )
57 simprr 733 . . . . . . . 8  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  F : U. J --> B )
58 fss 5477 . . . . . . . 8  |-  ( ( F : U. J --> B  /\  B  C_  Y
)  ->  F : U. J --> Y )
5957, 30, 58syl2anc 642 . . . . . . 7  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  F : U. J --> Y )
6059biantrurd 494 . . . . . 6  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( A. x  e.  K  ( `' F " x )  e.  J  <->  ( F : U. J --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) ) )
6140, 56, 603bitrrd 271 . . . . 5  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( ( F : U. J --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J )  <->  A. y  e.  ( Kt  B ) ( `' F " y )  e.  J ) )
6257biantrurd 494 . . . . 5  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( A. y  e.  ( Kt  B
) ( `' F " y )  e.  J  <->  ( F : U. J --> B  /\  A. y  e.  ( Kt  B ) ( `' F " y )  e.  J ) ) )
6361, 62bitrd 244 . . . 4  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( ( F : U. J --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J )  <->  ( F : U. J --> B  /\  A. y  e.  ( Kt  B ) ( `' F " y )  e.  J
) ) )
64 simprl 732 . . . . . 6  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  J  e.  Top )
6564, 16sylib 188 . . . . 5  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  J  e.  (TopOn `  U. J ) )
66 iscn 17065 . . . . 5  |-  ( ( J  e.  (TopOn `  U. J )  /\  K  e.  (TopOn `  Y )
)  ->  ( F  e.  ( J  Cn  K
)  <->  ( F : U. J --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) ) )
6765, 29, 66syl2anc 642 . . . 4  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( F  e.  ( J  Cn  K
)  <->  ( F : U. J --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) ) )
6819adantr 451 . . . . 5  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( Kt  B
)  e.  (TopOn `  B ) )
69 iscn 17065 . . . . 5  |-  ( ( J  e.  (TopOn `  U. J )  /\  ( Kt  B )  e.  (TopOn `  B ) )  -> 
( F  e.  ( J  Cn  ( Kt  B ) )  <->  ( F : U. J --> B  /\  A. y  e.  ( Kt  B ) ( `' F " y )  e.  J
) ) )
7065, 68, 69syl2anc 642 . . . 4  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( F  e.  ( J  Cn  ( Kt  B ) )  <->  ( F : U. J --> B  /\  A. y  e.  ( Kt  B ) ( `' F " y )  e.  J
) ) )
7163, 67, 703bitr4d 276 . . 3  |-  ( ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  /\  ( J  e.  Top  /\  F : U. J --> B ) )  ->  ( F  e.  ( J  Cn  K
)  <->  F  e.  ( J  Cn  ( Kt  B ) ) ) )
7271ex 423 . 2  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  (
( J  e.  Top  /\  F : U. J --> B )  ->  ( F  e.  ( J  Cn  K )  <->  F  e.  ( J  Cn  ( Kt  B ) ) ) ) )
7313, 25, 72pm5.21ndd 343 1  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  B  /\  B  C_  Y )  ->  ( F  e.  ( J  Cn  K )  <->  F  e.  ( J  Cn  ( Kt  B ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1642    e. wcel 1710   A.wral 2619   E.wrex 2620   _Vcvv 2864    i^i cin 3227    C_ wss 3228   U.cuni 3906   `'ccnv 4767   dom cdm 4768   ran crn 4769   "cima 4771   Fun wfun 5328    Fn wfn 5329   -->wf 5330   ` cfv 5334  (class class class)co 5942   ↾t crest 13418   Topctop 16731  TopOnctopon 16732    Cn ccn 17054
This theorem is referenced by:  cnrest2r  17115  rncmp  17223  conima  17251  concn  17252  kgencn2  17352  kgencn3  17353  qtoprest  17508  hmeores  17562  symgtgp  17880  submtmd  17883  subgtgp  17884  metdcn2  18441  metdscn2  18458  cnmptre  18523  iimulcn  18534  icchmeo  18537  evth  18555  evth2  18556  lebnumlem2  18558  reparphti  18593  efrlim  20369  rmulccn  23470  raddcn  23471  xrge0mulc1cn  23483  cvxpcon  24177  cvxscon  24178  cvmliftmolem1  24216  cvmliftlem8  24227  cvmlift2lem9  24246  cvmlift3lem6  24259  areacirclem4  25519  ivthALT  25582  cnres2  25806  cnresima  25807  refsumcn  27024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4210  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-int 3942  df-iun 3986  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-1st 6206  df-2nd 6207  df-recs 6472  df-rdg 6507  df-oadd 6567  df-er 6744  df-map 6859  df-en 6949  df-fin 6952  df-fi 7252  df-rest 13420  df-topgen 13437  df-top 16736  df-bases 16738  df-topon 16739  df-cn 17057
  Copyright terms: Public domain W3C validator