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	$⊢ φ \to K \in Haus$
	hauseqlcld.f	$⊢ φ \to F \in (J Cn K)$
	hauseqlcld.g	$⊢ φ \to G \in (J Cn K)$
Assertion	hauseqlcld	$⊢ φ \to dom (F \cap G) \in Clsd (J)$

Proof

Step	Hyp	Ref	Expression
1		hauseqlcld.k	$⊢ φ \to K \in Haus$
2		hauseqlcld.f	$⊢ φ \to F \in (J Cn K)$
3		hauseqlcld.g	$⊢ φ \to G \in (J Cn K)$
4		eqid	$⊢ ⋃ J = ⋃ J$
5		eqid	$⊢ ⋃ K = ⋃ K$
6	4 5	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
7	2 6	syl	$⊢ φ \to F : ⋃ J ⟶ ⋃ K$
8	7	ffvelrnda	$⊢ (φ \land b \in ⋃ J) \to F (b) \in ⋃ K$
9	8	biantrurd	$⊢ (φ \land b \in ⋃ J) \to (⟨F (b), G (b)⟩ \in I \leftrightarrow (F (b) \in ⋃ K \land ⟨F (b), G (b)⟩ \in I))$
10		fvex	$⊢ G (b) \in V$
11	10	ideq	$⊢ F (b) I G (b) \leftrightarrow F (b) = G (b)$
12		df-br	$⊢ F (b) I G (b) \leftrightarrow ⟨F (b), G (b)⟩ \in I$
13	11 12	bitr3i	$⊢ F (b) = G (b) \leftrightarrow ⟨F (b), G (b)⟩ \in I$
14	10	opelresi	$⊢ ⟨F (b), G (b)⟩ \in ({I ↾}_{⋃ K}) \leftrightarrow (F (b) \in ⋃ K \land ⟨F (b), G (b)⟩ \in I)$
15	9 13 14	3bitr4g	$⊢ (φ \land b \in ⋃ J) \to (F (b) = G (b) \leftrightarrow ⟨F (b), G (b)⟩ \in ({I ↾}_{⋃ K}))$
16		fveq2	$⊢ a = b \to F (a) = F (b)$
17		fveq2	$⊢ a = b \to G (a) = G (b)$
18	16 17	opeq12d	$⊢ a = b \to ⟨F (a), G (a)⟩ = ⟨F (b), G (b)⟩$
19		eqid	$⊢ (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) = (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩)$
20		opex	$⊢ ⟨F (b), G (b)⟩ \in V$
21	18 19 20	fvmpt	$⊢ b \in ⋃ J \to (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) (b) = ⟨F (b), G (b)⟩$
22	21	adantl	$⊢ (φ \land b \in ⋃ J) \to (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) (b) = ⟨F (b), G (b)⟩$
23	22	eleq1d	$⊢ (φ \land b \in ⋃ J) \to ((a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) (b) \in ({I ↾}_{⋃ K}) \leftrightarrow ⟨F (b), G (b)⟩ \in ({I ↾}_{⋃ K}))$
24	15 23	bitr4d	$⊢ (φ \land b \in ⋃ J) \to (F (b) = G (b) \leftrightarrow (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) (b) \in ({I ↾}_{⋃ K}))$
25	24	pm5.32da	$⊢ φ \to ((b \in ⋃ J \land F (b) = G (b)) \leftrightarrow (b \in ⋃ J \land (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) (b) \in ({I ↾}_{⋃ K})))$
26	7	ffnd	$⊢ φ \to F Fn ⋃ J$
27	4 5	cnf	$⊢ G \in (J Cn K) \to G : ⋃ J ⟶ ⋃ K$
28	3 27	syl	$⊢ φ \to G : ⋃ J ⟶ ⋃ K$
29	28	ffnd	$⊢ φ \to G Fn ⋃ J$
30		fndmin	$⊢ (F Fn ⋃ J \land G Fn ⋃ J) \to dom (F \cap G) = \{b \in ⋃ J \| F (b) = G (b)\}$
31	26 29 30	syl2anc	$⊢ φ \to dom (F \cap G) = \{b \in ⋃ J \| F (b) = G (b)\}$
32	31	eleq2d	$⊢ φ \to (b \in dom (F \cap G) \leftrightarrow b \in \{b \in ⋃ J \| F (b) = G (b)\})$
33		rabid	$⊢ b \in \{b \in ⋃ J \| F (b) = G (b)\} \leftrightarrow (b \in ⋃ J \land F (b) = G (b))$
34	32 33	bitrdi	$⊢ φ \to (b \in dom (F \cap G) \leftrightarrow (b \in ⋃ J \land F (b) = G (b)))$
35		opex	$⊢ ⟨F (a), G (a)⟩ \in V$
36	35 19	fnmpti	$⊢ (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) Fn ⋃ J$
37		elpreima	$⊢ (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) Fn ⋃ J \to (b \in {(a \in ⋃ J ⟼ ⟨F (a), G (a)⟩)}^{-1} [{I ↾}_{⋃ K}] \leftrightarrow (b \in ⋃ J \land (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) (b) \in ({I ↾}_{⋃ K})))$
38	36 37	mp1i	$⊢ φ \to (b \in {(a \in ⋃ J ⟼ ⟨F (a), G (a)⟩)}^{-1} [{I ↾}_{⋃ K}] \leftrightarrow (b \in ⋃ J \land (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) (b) \in ({I ↾}_{⋃ K})))$
39	25 34 38	3bitr4d	$⊢ φ \to (b \in dom (F \cap G) \leftrightarrow b \in {(a \in ⋃ J ⟼ ⟨F (a), G (a)⟩)}^{-1} [{I ↾}_{⋃ K}])$
40	39	eqrdv	$⊢ φ \to dom (F \cap G) = {(a \in ⋃ J ⟼ ⟨F (a), G (a)⟩)}^{-1} [{I ↾}_{⋃ K}]$
41	4 19	txcnmpt	$⊢ (F \in (J Cn K) \land G \in (J Cn K)) \to (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) \in (J Cn (K \times_{t} K))$
42	2 3 41	syl2anc	$⊢ φ \to (a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) \in (J Cn (K \times_{t} K))$
43	5	hausdiag	$⊢ K \in Haus \leftrightarrow (K \in Top \land {I ↾}_{⋃ K} \in Clsd (K \times_{t} K))$
44	43	simprbi	$⊢ K \in Haus \to {I ↾}_{⋃ K} \in Clsd (K \times_{t} K)$
45	1 44	syl	$⊢ φ \to {I ↾}_{⋃ K} \in Clsd (K \times_{t} K)$
46		cnclima	$⊢ ((a \in ⋃ J ⟼ ⟨F (a), G (a)⟩) \in (J Cn (K \times_{t} K)) \land {I ↾}_{⋃ K} \in Clsd (K \times_{t} K)) \to {(a \in ⋃ J ⟼ ⟨F (a), G (a)⟩)}^{-1} [{I ↾}_{⋃ K}] \in Clsd (J)$
47	42 45 46	syl2anc	$⊢ φ \to {(a \in ⋃ J ⟼ ⟨F (a), G (a)⟩)}^{-1} [{I ↾}_{⋃ K}] \in Clsd (J)$
48	40 47	eqeltrd	$⊢ φ \to dom (F \cap G) \in Clsd (J)$

Metamath Proof Explorer

Theorem hauseqlcld

Proof