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 = U. J
hauseqcn.k 
|- ( ph -> K e. Haus )
hauseqcn.f 
|- ( ph -> F e. ( J Cn K ) )
hauseqcn.g 
|- ( ph -> G e. ( J Cn K ) )
hauseqcn.e 
|- ( ph -> ( F |` A ) = ( G |` A ) )
hauseqcn.a 
|- ( ph -> A C_ X )
hauseqcn.c 
|- ( ph -> ( ( cls ` J ) ` A ) = X )
Assertion hauseqcn 
|- ( ph -> F = G )

Proof

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