Metamath Proof Explorer


Theorem hauseqcn

Description: In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28-Dec-2017)

Ref Expression
Hypotheses hauseqcn.x X = J
hauseqcn.k φ K Haus
hauseqcn.f φ F J Cn K
hauseqcn.g φ G J Cn K
hauseqcn.e φ F A = G A
hauseqcn.a φ A X
hauseqcn.c φ cls J A = X
Assertion hauseqcn φ F = G

Proof

Step Hyp Ref Expression
1 hauseqcn.x X = J
2 hauseqcn.k φ K Haus
3 hauseqcn.f φ F J Cn K
4 hauseqcn.g φ G J Cn K
5 hauseqcn.e φ F A = G A
6 hauseqcn.a φ A X
7 hauseqcn.c φ cls J A = X
8 cntop1 F J Cn K J Top
9 3 8 syl φ J Top
10 dmin dom F G dom F dom G
11 eqid J = J
12 eqid K = K
13 11 12 cnf F J Cn K F : J K
14 fdm F : J K dom F = J
15 3 13 14 3syl φ dom F = J
16 11 12 cnf G J Cn K G : J K
17 fdm G : J K dom G = J
18 4 16 17 3syl φ dom G = J
19 15 18 ineq12d φ dom F dom G = J J
20 inidm J J = J
21 19 20 eqtrdi φ dom F dom G = J
22 10 21 sseqtrid φ dom F G J
23 ffn F : J K F Fn J
24 3 13 23 3syl φ F Fn J
25 ffn G : J K G Fn J
26 4 16 25 3syl φ G Fn J
27 6 1 sseqtrdi φ A J
28 fnreseql F Fn J G Fn J A J F A = G A A dom F G
29 24 26 27 28 syl3anc φ F A = G A A dom F G
30 5 29 mpbid φ A dom F G
31 11 clsss J Top dom F G J A dom F G cls J A cls J dom F G
32 9 22 30 31 syl3anc φ cls J A cls J dom F G
33 2 3 4 hauseqlcld φ dom F G Clsd J
34 cldcls dom F G Clsd J cls J dom F G = dom F G
35 33 34 syl φ cls J dom F G = dom F G
36 32 7 35 3sstr3d φ X dom F G
37 1 36 eqsstrrid φ J dom F G
38 fneqeql2 F Fn J G Fn J F = G J dom F G
39 24 26 38 syl2anc φ F = G J dom F G
40 37 39 mpbird φ F = G