Metamath Proof Explorer

Theorem hausgraph

Description: The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion hausgraph 
|- ( ( K e. Haus /\ F e. ( J Cn K ) ) -> F e. ( Clsd ` ( J tX K ) ) )

Proof

Step Hyp Ref Expression
1 f1stres 
 |-  ( 1st |` ( U. J X. U. K ) ) : ( U. J X. U. K ) --> U. J
2 ffn 
 |-  ( ( 1st |` ( U. J X. U. K ) ) : ( U. J X. U. K ) --> U. J -> ( 1st |` ( U. J X. U. K ) ) Fn ( U. J X. U. K ) )
3 1 2 ax-mp 
 |-  ( 1st |` ( U. J X. U. K ) ) Fn ( U. J X. U. K )
4 fvco2 
 |-  ( ( ( 1st |` ( U. J X. U. K ) ) Fn ( U. J X. U. K ) /\ a e. ( U. J X. U. K ) ) -> ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) ` a ) = ( F ` ( ( 1st |` ( U. J X. U. K ) ) ` a ) ) )
5 3 4 mpan 
 |-  ( a e. ( U. J X. U. K ) -> ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) ` a ) = ( F ` ( ( 1st |` ( U. J X. U. K ) ) ` a ) ) )
6 5 adantl 
 |-  ( ( ( K e. Haus /\ F e. ( J Cn K ) ) /\ a e. ( U. J X. U. K ) ) -> ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) ` a ) = ( F ` ( ( 1st |` ( U. J X. U. K ) ) ` a ) ) )
7 fvres 
 |-  ( a e. ( U. J X. U. K ) -> ( ( 1st |` ( U. J X. U. K ) ) ` a ) = ( 1st ` a ) )
8 7 fveq2d 
 |-  ( a e. ( U. J X. U. K ) -> ( F ` ( ( 1st |` ( U. J X. U. K ) ) ` a ) ) = ( F ` ( 1st ` a ) ) )
9 8 adantl 
 |-  ( ( ( K e. Haus /\ F e. ( J Cn K ) ) /\ a e. ( U. J X. U. K ) ) -> ( F ` ( ( 1st |` ( U. J X. U. K ) ) ` a ) ) = ( F ` ( 1st ` a ) ) )
10 6 9 eqtrd 
 |-  ( ( ( K e. Haus /\ F e. ( J Cn K ) ) /\ a e. ( U. J X. U. K ) ) -> ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) ` a ) = ( F ` ( 1st ` a ) ) )
11 fvres 
 |-  ( a e. ( U. J X. U. K ) -> ( ( 2nd |` ( U. J X. U. K ) ) ` a ) = ( 2nd ` a ) )
12 11 adantl 
 |-  ( ( ( K e. Haus /\ F e. ( J Cn K ) ) /\ a e. ( U. J X. U. K ) ) -> ( ( 2nd |` ( U. J X. U. K ) ) ` a ) = ( 2nd ` a ) )
13 10 12 eqeq12d 
 |-  ( ( ( K e. Haus /\ F e. ( J Cn K ) ) /\ a e. ( U. J X. U. K ) ) -> ( ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) ` a ) = ( ( 2nd |` ( U. J X. U. K ) ) ` a ) <-> ( F ` ( 1st ` a ) ) = ( 2nd ` a ) ) )
14 13 rabbidva 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> { a e. ( U. J X. U. K ) | ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) ` a ) = ( ( 2nd |` ( U. J X. U. K ) ) ` a ) } = { a e. ( U. J X. U. K ) | ( F ` ( 1st ` a ) ) = ( 2nd ` a ) } )
15 eqid 
 |-  U. J = U. J
16 eqid 
 |-  U. K = U. K
17 15 16 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
18 17 adantl 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> F : U. J --> U. K )
19 fco 
 |-  ( ( F : U. J --> U. K /\ ( 1st |` ( U. J X. U. K ) ) : ( U. J X. U. K ) --> U. J ) -> ( F o. ( 1st |` ( U. J X. U. K ) ) ) : ( U. J X. U. K ) --> U. K )
20 18 1 19 sylancl 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> ( F o. ( 1st |` ( U. J X. U. K ) ) ) : ( U. J X. U. K ) --> U. K )
21 20 ffnd 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> ( F o. ( 1st |` ( U. J X. U. K ) ) ) Fn ( U. J X. U. K ) )
22 f2ndres 
 |-  ( 2nd |` ( U. J X. U. K ) ) : ( U. J X. U. K ) --> U. K
23 ffn 
 |-  ( ( 2nd |` ( U. J X. U. K ) ) : ( U. J X. U. K ) --> U. K -> ( 2nd |` ( U. J X. U. K ) ) Fn ( U. J X. U. K ) )
24 22 23 ax-mp 
 |-  ( 2nd |` ( U. J X. U. K ) ) Fn ( U. J X. U. K )
25 fndmin 
 |-  ( ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) Fn ( U. J X. U. K ) /\ ( 2nd |` ( U. J X. U. K ) ) Fn ( U. J X. U. K ) ) -> dom ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) i^i ( 2nd |` ( U. J X. U. K ) ) ) = { a e. ( U. J X. U. K ) | ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) ` a ) = ( ( 2nd |` ( U. J X. U. K ) ) ` a ) } )
26 21 24 25 sylancl 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> dom ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) i^i ( 2nd |` ( U. J X. U. K ) ) ) = { a e. ( U. J X. U. K ) | ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) ` a ) = ( ( 2nd |` ( U. J X. U. K ) ) ` a ) } )
27 fgraphxp 
 |-  ( F : U. J --> U. K -> F = { a e. ( U. J X. U. K ) | ( F ` ( 1st ` a ) ) = ( 2nd ` a ) } )
28 18 27 syl 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> F = { a e. ( U. J X. U. K ) | ( F ` ( 1st ` a ) ) = ( 2nd ` a ) } )
29 14 26 28 3eqtr4rd 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> F = dom ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) i^i ( 2nd |` ( U. J X. U. K ) ) ) )
30 simpl 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> K e. Haus )
31 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
32 31 adantl 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> J e. Top )
33 15 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
34 32 33 sylib 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> J e. ( TopOn ` U. J ) )
35 haustop 
 |-  ( K e. Haus -> K e. Top )
36 30 35 syl 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> K e. Top )
37 16 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
38 36 37 sylib 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> K e. ( TopOn ` U. K ) )
39 tx1cn 
 |-  ( ( J e. ( TopOn ` U. J ) /\ K e. ( TopOn ` U. K ) ) -> ( 1st |` ( U. J X. U. K ) ) e. ( ( J tX K ) Cn J ) )
40 34 38 39 syl2anc 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> ( 1st |` ( U. J X. U. K ) ) e. ( ( J tX K ) Cn J ) )
41 cnco 
 |-  ( ( ( 1st |` ( U. J X. U. K ) ) e. ( ( J tX K ) Cn J ) /\ F e. ( J Cn K ) ) -> ( F o. ( 1st |` ( U. J X. U. K ) ) ) e. ( ( J tX K ) Cn K ) )
42 40 41 sylancom 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> ( F o. ( 1st |` ( U. J X. U. K ) ) ) e. ( ( J tX K ) Cn K ) )
43 tx2cn 
 |-  ( ( J e. ( TopOn ` U. J ) /\ K e. ( TopOn ` U. K ) ) -> ( 2nd |` ( U. J X. U. K ) ) e. ( ( J tX K ) Cn K ) )
44 34 38 43 syl2anc 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> ( 2nd |` ( U. J X. U. K ) ) e. ( ( J tX K ) Cn K ) )
45 30 42 44 hauseqlcld 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> dom ( ( F o. ( 1st |` ( U. J X. U. K ) ) ) i^i ( 2nd |` ( U. J X. U. K ) ) ) e. ( Clsd ` ( J tX K ) ) )
46 29 45 eqeltrd 
 |-  ( ( K e. Haus /\ F e. ( J Cn K ) ) -> F e. ( Clsd ` ( J tX K ) ) )