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 \in Haus \land F \in (J Cn K)) \to F \in Clsd (J \times_{t} K)$

Proof

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

Metamath Proof Explorer

Theorem hausgraph

Proof