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

Theorem cnextf 21081
 Description: Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017.)
Hypotheses
Ref Expression
cnextf.1
cnextf.2
cnextf.3
cnextf.4
cnextf.5
cnextf.a
cnextf.6
cnextf.7 t
Assertion
Ref Expression
cnextf CnExt
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,

Proof of Theorem cnextf
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cnextf.3 . . . 4
2 cnextf.4 . . . 4
3 cnextf.5 . . . 4
4 cnextf.a . . . 4
5 cnextf.1 . . . . 5
6 cnextf.2 . . . . 5
75, 6cnextfun 21079 . . . 4 CnExt
81, 2, 3, 4, 7syl22anc 1269 . . 3 CnExt
9 simpl 459 . . . . . . 7
10 cnextf.6 . . . . . . . . 9
1110eleq2d 2514 . . . . . . . 8
1211biimpar 488 . . . . . . 7
13 cnextf.7 . . . . . . . 8 t
14 n0 3741 . . . . . . . 8 t t
1513, 14sylib 200 . . . . . . 7 t
16 haustop 20347 . . . . . . . . . . . . . 14
172, 16syl 17 . . . . . . . . . . . . 13
185, 6cnextfval 21077 . . . . . . . . . . . . 13 CnExt t
191, 17, 3, 4, 18syl22anc 1269 . . . . . . . . . . . 12 CnExt t
2019eleq2d 2514 . . . . . . . . . . 11 CnExt t
21 opeliunxp 4886 . . . . . . . . . . 11 t t
2220, 21syl6bb 265 . . . . . . . . . 10 CnExt t
2322exbidv 1768 . . . . . . . . 9 CnExt t
24 19.42v 1834 . . . . . . . . 9 t t
2523, 24syl6bb 265 . . . . . . . 8 CnExt t
2625biimpar 488 . . . . . . 7 t CnExt
279, 12, 15, 26syl12anc 1266 . . . . . 6 CnExt
2825simprbda 629 . . . . . . 7 CnExt
2911adantr 467 . . . . . . 7 CnExt
3028, 29mpbid 214 . . . . . 6 CnExt
3127, 30impbida 843 . . . . 5 CnExt
3231abbi2dv 2570 . . . 4 CnExt
33 dfdm3 5022 . . . 4 CnExt CnExt
3432, 33syl6reqr 2504 . . 3 CnExt
35 df-fn 5585 . . 3 CnExt CnExt CnExt
368, 34, 35sylanbrc 670 . 2 CnExt
3719rneqd 5062 . . 3 CnExt t
38 rniun 5246 . . . 4 t t
39 vex 3048 . . . . . . . . 9
4039snnz 4090 . . . . . . . 8
41 rnxp 5267 . . . . . . . 8 t t
4240, 41ax-mp 5 . . . . . . 7 t t
4311biimpa 487 . . . . . . . 8
446toptopon 19948 . . . . . . . . . . 11 TopOn
4517, 44sylib 200 . . . . . . . . . 10 TopOn
4645adantr 467 . . . . . . . . 9 TopOn
475toptopon 19948 . . . . . . . . . . . 12 TopOn
481, 47sylib 200 . . . . . . . . . . 11 TopOn
4948adantr 467 . . . . . . . . . 10 TopOn
504adantr 467 . . . . . . . . . 10
51 simpr 463 . . . . . . . . . 10
52 trnei 20907 . . . . . . . . . . 11 TopOn t
5352biimpa 487 . . . . . . . . . 10 TopOn t
5449, 50, 51, 12, 53syl31anc 1271 . . . . . . . . 9 t
553adantr 467 . . . . . . . . 9
56 flfelbas 21009 . . . . . . . . . . 11 TopOn t t
5756ex 436 . . . . . . . . . 10 TopOn t t
5857ssrdv 3438 . . . . . . . . 9 TopOn t t
5946, 54, 55, 58syl3anc 1268 . . . . . . . 8 t
6043, 59syldan 473 . . . . . . 7 t
6142, 60syl5eqss 3476 . . . . . 6 t
6261ralrimiva 2802 . . . . 5 t
63 iunss 4319 . . . . 5 t t
6462, 63sylibr 216 . . . 4 t
6538, 64syl5eqss 3476 . . 3 t
6637, 65eqsstrd 3466 . 2 CnExt
67 df-f 5586 . 2 CnExt CnExt CnExt
6836, 66, 67sylanbrc 670 1 CnExt
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 985   wceq 1444  wex 1663   wcel 1887  cab 2437   wne 2622  wral 2737   wss 3404  c0 3731  csn 3968  cop 3974  cuni 4198  ciun 4278   cxp 4832   cdm 4834   crn 4835   wfun 5576   wfn 5577  wf 5578  cfv 5582  (class class class)co 6290   ↾t crest 15319  ctop 19917  TopOnctopon 19918  ccl 20033  cnei 20113  cha 20324  cfil 20860   cflf 20950  CnExtccnext 21074 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-iin 4281  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-map 7474  df-pm 7475  df-rest 15321  df-fbas 18967  df-fg 18968  df-top 19921  df-topon 19923  df-cld 20034  df-ntr 20035  df-cls 20036  df-nei 20114  df-haus 20331  df-fil 20861  df-fm 20953  df-flim 20954  df-flf 20955  df-cnext 21075 This theorem is referenced by:  cnextcn  21082  cnextfres1  21083
 Copyright terms: Public domain W3C validator