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 ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 ∈ ( Clsd ‘ ( 𝐽 ×t 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 f1stres ⊢ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) : ( ∪ 𝐽 × ∪ 𝐾 ) ⟶ ∪ 𝐽
2 ffn ⊢ ( ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) : ( ∪ 𝐽 × ∪ 𝐾 ) ⟶ ∪ 𝐽 → ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) Fn ( ∪ 𝐽 × ∪ 𝐾 ) )
3 1 2 ax-mp ⊢ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) Fn ( ∪ 𝐽 × ∪ 𝐾 )
4 fvco2 ⊢ ( ( ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) Fn ( ∪ 𝐽 × ∪ 𝐾 ) ∧ 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ) → ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ‘ 𝑎 ) = ( 𝐹 ‘ ( ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) ) )
5 3 4 mpan ⊢ ( 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) → ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ‘ 𝑎 ) = ( 𝐹 ‘ ( ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) ) )
6 5 adantl ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ) → ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ‘ 𝑎 ) = ( 𝐹 ‘ ( ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) ) )
7 fvres ⊢ ( 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) → ( ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) = ( 1st ‘ 𝑎 ) )
8 7 fveq2d ⊢ ( 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) → ( 𝐹 ‘ ( ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) ) = ( 𝐹 ‘ ( 1st ‘ 𝑎 ) ) )
9 8 adantl ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ) → ( 𝐹 ‘ ( ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) ) = ( 𝐹 ‘ ( 1st ‘ 𝑎 ) ) )
10 6 9 eqtrd ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ) → ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ‘ 𝑎 ) = ( 𝐹 ‘ ( 1st ‘ 𝑎 ) ) )
11 fvres ⊢ ( 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) → ( ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) = ( 2nd ‘ 𝑎 ) )
12 11 adantl ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ) → ( ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) = ( 2nd ‘ 𝑎 ) )
13 10 12 eqeq12d ⊢ ( ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ) → ( ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ‘ 𝑎 ) = ( ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) ↔ ( 𝐹 ‘ ( 1st ‘ 𝑎 ) ) = ( 2nd ‘ 𝑎 ) ) )
14 13 rabbidva ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → { 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ∣ ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ‘ 𝑎 ) = ( ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) } = { 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ∣ ( 𝐹 ‘ ( 1st ‘ 𝑎 ) ) = ( 2nd ‘ 𝑎 ) } )
15 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
16 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
17 15 16 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
18 17 adantl ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
19 fco ⊢ ( ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) : ( ∪ 𝐽 × ∪ 𝐾 ) ⟶ ∪ 𝐽 ) → ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) : ( ∪ 𝐽 × ∪ 𝐾 ) ⟶ ∪ 𝐾 )
20 18 1 19 sylancl ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) : ( ∪ 𝐽 × ∪ 𝐾 ) ⟶ ∪ 𝐾 )
21 20 ffnd ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) Fn ( ∪ 𝐽 × ∪ 𝐾 ) )
22 f2ndres ⊢ ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) : ( ∪ 𝐽 × ∪ 𝐾 ) ⟶ ∪ 𝐾
23 ffn ⊢ ( ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) : ( ∪ 𝐽 × ∪ 𝐾 ) ⟶ ∪ 𝐾 → ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) Fn ( ∪ 𝐽 × ∪ 𝐾 ) )
24 22 23 ax-mp ⊢ ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) Fn ( ∪ 𝐽 × ∪ 𝐾 )
25 fndmin ⊢ ( ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) Fn ( ∪ 𝐽 × ∪ 𝐾 ) ∧ ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) Fn ( ∪ 𝐽 × ∪ 𝐾 ) ) → dom ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ∩ ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) = { 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ∣ ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ‘ 𝑎 ) = ( ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) } )
26 21 24 25 sylancl ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → dom ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ∩ ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) = { 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ∣ ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ‘ 𝑎 ) = ( ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ‘ 𝑎 ) } )
27 fgraphxp ⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → 𝐹 = { 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ∣ ( 𝐹 ‘ ( 1st ‘ 𝑎 ) ) = ( 2nd ‘ 𝑎 ) } )
28 18 27 syl ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 = { 𝑎 ∈ ( ∪ 𝐽 × ∪ 𝐾 ) ∣ ( 𝐹 ‘ ( 1st ‘ 𝑎 ) ) = ( 2nd ‘ 𝑎 ) } )
29 14 26 28 3eqtr4rd ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 = dom ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ∩ ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) )
30 simpl ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Haus )
31 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
32 31 adantl ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Top )
33 15 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
34 32 33 sylib ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
35 haustop ⊢ ( 𝐾 ∈ Haus → 𝐾 ∈ Top )
36 30 35 syl ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Top )
37 16 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
38 36 37 sylib ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
39 tx1cn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) → ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) )
40 34 38 39 syl2anc ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) )
41 cnco ⊢ ( ( ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )
42 40 41 sylancom ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )
43 tx2cn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) → ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )
44 34 38 43 syl2anc ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )
45 30 42 44 hauseqlcld ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → dom ( ( 𝐹 ∘ ( 1st ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ∩ ( 2nd ↾ ( ∪ 𝐽 × ∪ 𝐾 ) ) ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐾 ) ) )
46 29 45 eqeltrd ⊢ ( ( 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 ∈ ( Clsd ‘ ( 𝐽 ×t 𝐾 ) ) )