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 
|- ( ph -> K e. Haus )
hauseqlcld.f 
|- ( ph -> F e. ( J Cn K ) )
hauseqlcld.g 
|- ( ph -> G e. ( J Cn K ) )
Assertion hauseqlcld 
|- ( ph -> dom ( F i^i G ) e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 hauseqlcld.k 
 |-  ( ph -> K e. Haus )
2 hauseqlcld.f 
 |-  ( ph -> F e. ( J Cn K ) )
3 hauseqlcld.g 
 |-  ( ph -> G e. ( J Cn K ) )
4 eqid 
 |-  U. J = U. J
5 eqid 
 |-  U. K = U. K
6 4 5 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
7 2 6 syl 
 |-  ( ph -> F : U. J --> U. K )
8 7 ffvelrnda 
 |-  ( ( ph /\ b e. U. J ) -> ( F ` b ) e. U. K )
9 8 biantrurd 
 |-  ( ( ph /\ b e. U. J ) -> ( <. ( F ` b ) , ( G ` b ) >. e. _I <-> ( ( F ` b ) e. U. K /\ <. ( F ` b ) , ( G ` b ) >. e. _I ) ) )
10 fvex 
 |-  ( G ` b ) e. _V
11 10 ideq 
 |-  ( ( F ` b ) _I ( G ` b ) <-> ( F ` b ) = ( G ` b ) )
12 df-br 
 |-  ( ( F ` b ) _I ( G ` b ) <-> <. ( F ` b ) , ( G ` b ) >. e. _I )
13 11 12 bitr3i 
 |-  ( ( F ` b ) = ( G ` b ) <-> <. ( F ` b ) , ( G ` b ) >. e. _I )
14 10 opelresi 
 |-  ( <. ( F ` b ) , ( G ` b ) >. e. ( _I |` U. K ) <-> ( ( F ` b ) e. U. K /\ <. ( F ` b ) , ( G ` b ) >. e. _I ) )
15 9 13 14 3bitr4g 
 |-  ( ( ph /\ b e. U. J ) -> ( ( F ` b ) = ( G ` b ) <-> <. ( F ` b ) , ( G ` b ) >. e. ( _I |` U. K ) ) )
16 fveq2 
 |-  ( a = b -> ( F ` a ) = ( F ` b ) )
17 fveq2 
 |-  ( a = b -> ( G ` a ) = ( G ` b ) )
18 16 17 opeq12d 
 |-  ( a = b -> <. ( F ` a ) , ( G ` a ) >. = <. ( F ` b ) , ( G ` b ) >. )
19 eqid 
 |-  ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) = ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. )
20 opex 
 |-  <. ( F ` b ) , ( G ` b ) >. e. _V
21 18 19 20 fvmpt 
 |-  ( b e. U. J -> ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) = <. ( F ` b ) , ( G ` b ) >. )
22 21 adantl 
 |-  ( ( ph /\ b e. U. J ) -> ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) = <. ( F ` b ) , ( G ` b ) >. )
23 22 eleq1d 
 |-  ( ( ph /\ b e. U. J ) -> ( ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) <-> <. ( F ` b ) , ( G ` b ) >. e. ( _I |` U. K ) ) )
24 15 23 bitr4d 
 |-  ( ( ph /\ b e. U. J ) -> ( ( F ` b ) = ( G ` b ) <-> ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) ) )
25 24 pm5.32da 
 |-  ( ph -> ( ( b e. U. J /\ ( F ` b ) = ( G ` b ) ) <-> ( b e. U. J /\ ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) ) ) )
26 7 ffnd 
 |-  ( ph -> F Fn U. J )
27 4 5 cnf 
 |-  ( G e. ( J Cn K ) -> G : U. J --> U. K )
28 3 27 syl 
 |-  ( ph -> G : U. J --> U. K )
29 28 ffnd 
 |-  ( ph -> G Fn U. J )
30 fndmin 
 |-  ( ( F Fn U. J /\ G Fn U. J ) -> dom ( F i^i G ) = { b e. U. J | ( F ` b ) = ( G ` b ) } )
31 26 29 30 syl2anc 
 |-  ( ph -> dom ( F i^i G ) = { b e. U. J | ( F ` b ) = ( G ` b ) } )
32 31 eleq2d 
 |-  ( ph -> ( b e. dom ( F i^i G ) <-> b e. { b e. U. J | ( F ` b ) = ( G ` b ) } ) )
33 rabid 
 |-  ( b e. { b e. U. J | ( F ` b ) = ( G ` b ) } <-> ( b e. U. J /\ ( F ` b ) = ( G ` b ) ) )
34 32 33 bitrdi 
 |-  ( ph -> ( b e. dom ( F i^i G ) <-> ( b e. U. J /\ ( F ` b ) = ( G ` b ) ) ) )
35 opex 
 |-  <. ( F ` a ) , ( G ` a ) >. e. _V
36 35 19 fnmpti 
 |-  ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) Fn U. J
37 elpreima 
 |-  ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) Fn U. J -> ( b e. ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) <-> ( b e. U. J /\ ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) ) ) )
38 36 37 mp1i 
 |-  ( ph -> ( b e. ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) <-> ( b e. U. J /\ ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) ) ) )
39 25 34 38 3bitr4d 
 |-  ( ph -> ( b e. dom ( F i^i G ) <-> b e. ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) ) )
40 39 eqrdv 
 |-  ( ph -> dom ( F i^i G ) = ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) )
41 4 19 txcnmpt 
 |-  ( ( F e. ( J Cn K ) /\ G e. ( J Cn K ) ) -> ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) e. ( J Cn ( K tX K ) ) )
42 2 3 41 syl2anc 
 |-  ( ph -> ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) e. ( J Cn ( K tX K ) ) )
43 5 hausdiag 
 |-  ( K e. Haus <-> ( K e. Top /\ ( _I |` U. K ) e. ( Clsd ` ( K tX K ) ) ) )
44 43 simprbi 
 |-  ( K e. Haus -> ( _I |` U. K ) e. ( Clsd ` ( K tX K ) ) )
45 1 44 syl 
 |-  ( ph -> ( _I |` U. K ) e. ( Clsd ` ( K tX K ) ) )
46 cnclima 
 |-  ( ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) e. ( J Cn ( K tX K ) ) /\ ( _I |` U. K ) e. ( Clsd ` ( K tX K ) ) ) -> ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) e. ( Clsd ` J ) )
47 42 45 46 syl2anc 
 |-  ( ph -> ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) e. ( Clsd ` J ) )
48 40 47 eqeltrd 
 |-  ( ph -> dom ( F i^i G ) e. ( Clsd ` J ) )