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

Theorem hauseqlcld 20673
 Description: In a Hausdorff topology, the equalizer of two continuous functions is closed (thus, two continuous functions which agree on a dense set agree everywhere). (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
hauseqlcld.k
hauseqlcld.f
hauseqlcld.g
Assertion
Ref Expression
hauseqlcld

Proof of Theorem hauseqlcld
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hauseqlcld.f . . . . . . . . . 10
2 eqid 2453 . . . . . . . . . . 11
3 eqid 2453 . . . . . . . . . . 11
42, 3cnf 20274 . . . . . . . . . 10
51, 4syl 17 . . . . . . . . 9
65ffvelrnda 6027 . . . . . . . 8
76biantrud 510 . . . . . . 7
8 fvex 5880 . . . . . . . . 9
98ideq 4990 . . . . . . . 8
10 df-br 4406 . . . . . . . 8
119, 10bitr3i 255 . . . . . . 7
128opelres 5113 . . . . . . 7
137, 11, 123bitr4g 292 . . . . . 6
14 fveq2 5870 . . . . . . . . . 10
15 fveq2 5870 . . . . . . . . . 10
1614, 15opeq12d 4177 . . . . . . . . 9
17 eqid 2453 . . . . . . . . 9
18 opex 4667 . . . . . . . . 9
1916, 17, 18fvmpt 5953 . . . . . . . 8
2019adantl 468 . . . . . . 7
2120eleq1d 2515 . . . . . 6
2213, 21bitr4d 260 . . . . 5
2322pm5.32da 647 . . . 4
24 ffn 5733 . . . . . . . 8
255, 24syl 17 . . . . . . 7
26 hauseqlcld.g . . . . . . . . 9
272, 3cnf 20274 . . . . . . . . 9
2826, 27syl 17 . . . . . . . 8
29 ffn 5733 . . . . . . . 8
3028, 29syl 17 . . . . . . 7
31 fndmin 5994 . . . . . . 7
3225, 30, 31syl2anc 667 . . . . . 6
3332eleq2d 2516 . . . . 5
34 rabid 2969 . . . . 5
3533, 34syl6bb 265 . . . 4
36 opex 4667 . . . . . 6
3736, 17fnmpti 5711 . . . . 5
38 elpreima 6007 . . . . 5
3937, 38mp1i 13 . . . 4
4023, 35, 393bitr4d 289 . . 3
4140eqrdv 2451 . 2
422, 17txcnmpt 20651 . . . 4
431, 26, 42syl2anc 667 . . 3
44 hauseqlcld.k . . . 4
453hausdiag 20672 . . . . 5
4645simprbi 466 . . . 4
4744, 46syl 17 . . 3
48 cnclima 20296 . . 3
4943, 47, 48syl2anc 667 . 2
5041, 49eqeltrd 2531 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1446   wcel 1889  crab 2743   cin 3405  cop 3976  cuni 4201   class class class wbr 4405   cmpt 4464   cid 4747  ccnv 4836   cdm 4837   cres 4839  cima 4840   wfn 5580  wf 5581  cfv 5585  (class class class)co 6295  ctop 19929  ccld 20043   ccn 20252  cha 20336   ctx 20587 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-1st 6798  df-2nd 6799  df-map 7479  df-topgen 15354  df-top 19933  df-bases 19934  df-topon 19935  df-cld 20046  df-cn 20255  df-haus 20343  df-tx 20589 This theorem is referenced by:  hauseqcn  28713  hausgraph  36101
 Copyright terms: Public domain W3C validator