Metamath Proof Explorer


Theorem hauseqlcld

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)

Ref Expression
Hypotheses hauseqlcld.k ( 𝜑𝐾 ∈ Haus )
hauseqlcld.f ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
hauseqlcld.g ( 𝜑𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion hauseqlcld ( 𝜑 → dom ( 𝐹𝐺 ) ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 hauseqlcld.k ( 𝜑𝐾 ∈ Haus )
2 hauseqlcld.f ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3 hauseqlcld.g ( 𝜑𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
4 eqid 𝐽 = 𝐽
5 eqid 𝐾 = 𝐾
6 4 5 cnf ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝐽 𝐾 )
7 2 6 syl ( 𝜑𝐹 : 𝐽 𝐾 )
8 7 ffvelrnda ( ( 𝜑𝑏 𝐽 ) → ( 𝐹𝑏 ) ∈ 𝐾 )
9 8 biantrurd ( ( 𝜑𝑏 𝐽 ) → ( ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ ∈ I ↔ ( ( 𝐹𝑏 ) ∈ 𝐾 ∧ ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ ∈ I ) ) )
10 fvex ( 𝐺𝑏 ) ∈ V
11 10 ideq ( ( 𝐹𝑏 ) I ( 𝐺𝑏 ) ↔ ( 𝐹𝑏 ) = ( 𝐺𝑏 ) )
12 df-br ( ( 𝐹𝑏 ) I ( 𝐺𝑏 ) ↔ ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ ∈ I )
13 11 12 bitr3i ( ( 𝐹𝑏 ) = ( 𝐺𝑏 ) ↔ ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ ∈ I )
14 10 opelresi ( ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ ∈ ( I ↾ 𝐾 ) ↔ ( ( 𝐹𝑏 ) ∈ 𝐾 ∧ ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ ∈ I ) )
15 9 13 14 3bitr4g ( ( 𝜑𝑏 𝐽 ) → ( ( 𝐹𝑏 ) = ( 𝐺𝑏 ) ↔ ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ ∈ ( I ↾ 𝐾 ) ) )
16 fveq2 ( 𝑎 = 𝑏 → ( 𝐹𝑎 ) = ( 𝐹𝑏 ) )
17 fveq2 ( 𝑎 = 𝑏 → ( 𝐺𝑎 ) = ( 𝐺𝑏 ) )
18 16 17 opeq12d ( 𝑎 = 𝑏 → ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ = ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ )
19 eqid ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) = ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ )
20 opex ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ ∈ V
21 18 19 20 fvmpt ( 𝑏 𝐽 → ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ‘ 𝑏 ) = ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ )
22 21 adantl ( ( 𝜑𝑏 𝐽 ) → ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ‘ 𝑏 ) = ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ )
23 22 eleq1d ( ( 𝜑𝑏 𝐽 ) → ( ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ‘ 𝑏 ) ∈ ( I ↾ 𝐾 ) ↔ ⟨ ( 𝐹𝑏 ) , ( 𝐺𝑏 ) ⟩ ∈ ( I ↾ 𝐾 ) ) )
24 15 23 bitr4d ( ( 𝜑𝑏 𝐽 ) → ( ( 𝐹𝑏 ) = ( 𝐺𝑏 ) ↔ ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ‘ 𝑏 ) ∈ ( I ↾ 𝐾 ) ) )
25 24 pm5.32da ( 𝜑 → ( ( 𝑏 𝐽 ∧ ( 𝐹𝑏 ) = ( 𝐺𝑏 ) ) ↔ ( 𝑏 𝐽 ∧ ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ‘ 𝑏 ) ∈ ( I ↾ 𝐾 ) ) ) )
26 7 ffnd ( 𝜑𝐹 Fn 𝐽 )
27 4 5 cnf ( 𝐺 ∈ ( 𝐽 Cn 𝐾 ) → 𝐺 : 𝐽 𝐾 )
28 3 27 syl ( 𝜑𝐺 : 𝐽 𝐾 )
29 28 ffnd ( 𝜑𝐺 Fn 𝐽 )
30 fndmin ( ( 𝐹 Fn 𝐽𝐺 Fn 𝐽 ) → dom ( 𝐹𝐺 ) = { 𝑏 𝐽 ∣ ( 𝐹𝑏 ) = ( 𝐺𝑏 ) } )
31 26 29 30 syl2anc ( 𝜑 → dom ( 𝐹𝐺 ) = { 𝑏 𝐽 ∣ ( 𝐹𝑏 ) = ( 𝐺𝑏 ) } )
32 31 eleq2d ( 𝜑 → ( 𝑏 ∈ dom ( 𝐹𝐺 ) ↔ 𝑏 ∈ { 𝑏 𝐽 ∣ ( 𝐹𝑏 ) = ( 𝐺𝑏 ) } ) )
33 rabid ( 𝑏 ∈ { 𝑏 𝐽 ∣ ( 𝐹𝑏 ) = ( 𝐺𝑏 ) } ↔ ( 𝑏 𝐽 ∧ ( 𝐹𝑏 ) = ( 𝐺𝑏 ) ) )
34 32 33 bitrdi ( 𝜑 → ( 𝑏 ∈ dom ( 𝐹𝐺 ) ↔ ( 𝑏 𝐽 ∧ ( 𝐹𝑏 ) = ( 𝐺𝑏 ) ) ) )
35 opex ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ∈ V
36 35 19 fnmpti ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) Fn 𝐽
37 elpreima ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) Fn 𝐽 → ( 𝑏 ∈ ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) “ ( I ↾ 𝐾 ) ) ↔ ( 𝑏 𝐽 ∧ ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ‘ 𝑏 ) ∈ ( I ↾ 𝐾 ) ) ) )
38 36 37 mp1i ( 𝜑 → ( 𝑏 ∈ ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) “ ( I ↾ 𝐾 ) ) ↔ ( 𝑏 𝐽 ∧ ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ‘ 𝑏 ) ∈ ( I ↾ 𝐾 ) ) ) )
39 25 34 38 3bitr4d ( 𝜑 → ( 𝑏 ∈ dom ( 𝐹𝐺 ) ↔ 𝑏 ∈ ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) “ ( I ↾ 𝐾 ) ) ) )
40 39 eqrdv ( 𝜑 → dom ( 𝐹𝐺 ) = ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) “ ( I ↾ 𝐾 ) ) )
41 4 19 txcnmpt ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐾 ) ) )
42 2 3 41 syl2anc ( 𝜑 → ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐾 ) ) )
43 5 hausdiag ( 𝐾 ∈ Haus ↔ ( 𝐾 ∈ Top ∧ ( I ↾ 𝐾 ) ∈ ( Clsd ‘ ( 𝐾 ×t 𝐾 ) ) ) )
44 43 simprbi ( 𝐾 ∈ Haus → ( I ↾ 𝐾 ) ∈ ( Clsd ‘ ( 𝐾 ×t 𝐾 ) ) )
45 1 44 syl ( 𝜑 → ( I ↾ 𝐾 ) ∈ ( Clsd ‘ ( 𝐾 ×t 𝐾 ) ) )
46 cnclima ( ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐾 ) ) ∧ ( I ↾ 𝐾 ) ∈ ( Clsd ‘ ( 𝐾 ×t 𝐾 ) ) ) → ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) “ ( I ↾ 𝐾 ) ) ∈ ( Clsd ‘ 𝐽 ) )
47 42 45 46 syl2anc ( 𝜑 → ( ( 𝑎 𝐽 ↦ ⟨ ( 𝐹𝑎 ) , ( 𝐺𝑎 ) ⟩ ) “ ( I ↾ 𝐾 ) ) ∈ ( Clsd ‘ 𝐽 ) )
48 40 47 eqeltrd ( 𝜑 → dom ( 𝐹𝐺 ) ∈ ( Clsd ‘ 𝐽 ) )