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 ⊢ 𝑋 = ∪ 𝐽
hauseqcn.k ⊢ ( 𝜑 → 𝐾 ∈ Haus )
hauseqcn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
hauseqcn.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
hauseqcn.e ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) )
hauseqcn.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
hauseqcn.c ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
Assertion hauseqcn ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 hauseqcn.x ⊢ 𝑋 = ∪ 𝐽
2 hauseqcn.k ⊢ ( 𝜑 → 𝐾 ∈ Haus )
3 hauseqcn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 hauseqcn.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
5 hauseqcn.e ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) )
6 hauseqcn.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
7 hauseqcn.c ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
8 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
9 3 8 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
10 dmin ⊢ dom ( 𝐹 ∩ 𝐺 ) ⊆ ( dom 𝐹 ∩ dom 𝐺 )
11 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
12 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
13 11 12 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
14 fdm ⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → dom 𝐹 = ∪ 𝐽 )
15 3 13 14 3syl ⊢ ( 𝜑 → dom 𝐹 = ∪ 𝐽 )
16 11 12 cnf ⊢ ( 𝐺 ∈ ( 𝐽 Cn 𝐾 ) → 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 )
17 fdm ⊢ ( 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 → dom 𝐺 = ∪ 𝐽 )
18 4 16 17 3syl ⊢ ( 𝜑 → dom 𝐺 = ∪ 𝐽 )
19 15 18 ineq12d ⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) = ( ∪ 𝐽 ∩ ∪ 𝐽 ) )
20 inidm ⊢ ( ∪ 𝐽 ∩ ∪ 𝐽 ) = ∪ 𝐽
21 19 20 eqtrdi ⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) = ∪ 𝐽 )
22 10 21 sseqtrid ⊢ ( 𝜑 → dom ( 𝐹 ∩ 𝐺 ) ⊆ ∪ 𝐽 )
23 ffn ⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → 𝐹 Fn ∪ 𝐽 )
24 3 13 23 3syl ⊢ ( 𝜑 → 𝐹 Fn ∪ 𝐽 )
25 ffn ⊢ ( 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 → 𝐺 Fn ∪ 𝐽 )
26 4 16 25 3syl ⊢ ( 𝜑 → 𝐺 Fn ∪ 𝐽 )
27 6 1 sseqtrdi ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐽 )
28 fnreseql ⊢ ( ( 𝐹 Fn ∪ 𝐽 ∧ 𝐺 Fn ∪ 𝐽 ∧ 𝐴 ⊆ ∪ 𝐽 ) → ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ↔ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )
29 24 26 27 28 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ↔ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )
30 5 29 mpbid ⊢ ( 𝜑 → 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) )
31 11 clsss ⊢ ( ( 𝐽 ∈ Top ∧ dom ( 𝐹 ∩ 𝐺 ) ⊆ ∪ 𝐽 ∧ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ dom ( 𝐹 ∩ 𝐺 ) ) )
32 9 22 30 31 syl3anc ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ dom ( 𝐹 ∩ 𝐺 ) ) )
33 2 3 4 hauseqlcld ⊢ ( 𝜑 → dom ( 𝐹 ∩ 𝐺 ) ∈ ( Clsd ‘ 𝐽 ) )
34 cldcls ⊢ ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ dom ( 𝐹 ∩ 𝐺 ) ) = dom ( 𝐹 ∩ 𝐺 ) )
35 33 34 syl ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ dom ( 𝐹 ∩ 𝐺 ) ) = dom ( 𝐹 ∩ 𝐺 ) )
36 32 7 35 3sstr3d ⊢ ( 𝜑 → 𝑋 ⊆ dom ( 𝐹 ∩ 𝐺 ) )
37 1 36 eqsstrrid ⊢ ( 𝜑 → ∪ 𝐽 ⊆ dom ( 𝐹 ∩ 𝐺 ) )
38 fneqeql2 ⊢ ( ( 𝐹 Fn ∪ 𝐽 ∧ 𝐺 Fn ∪ 𝐽 ) → ( 𝐹 = 𝐺 ↔ ∪ 𝐽 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )
39 24 26 38 syl2anc ⊢ ( 𝜑 → ( 𝐹 = 𝐺 ↔ ∪ 𝐽 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )
40 37 39 mpbird ⊢ ( 𝜑 → 𝐹 = 𝐺 )