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 ‘ 𝐽 ) )