hauseqcn

Description: In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28-Dec-2017)

	Ref	Expression
Hypotheses	hauseqcn.x	$⊢ X = ⋃ J$
	hauseqcn.k	$⊢ φ \to K \in Haus$
	hauseqcn.f	$⊢ φ \to F \in (J Cn K)$
	hauseqcn.g	$⊢ φ \to G \in (J Cn K)$
	hauseqcn.e	$⊢ φ \to {F ↾}_{A} = {G ↾}_{A}$
	hauseqcn.a	$⊢ φ \to A \subseteq X$
	hauseqcn.c	$⊢ φ \to cls (J) (A) = X$
Assertion	hauseqcn	$⊢ φ \to F = G$

Proof

Step	Hyp	Ref	Expression
1		hauseqcn.x	$⊢ X = ⋃ J$
2		hauseqcn.k	$⊢ φ \to K \in Haus$
3		hauseqcn.f	$⊢ φ \to F \in (J Cn K)$
4		hauseqcn.g	$⊢ φ \to G \in (J Cn K)$
5		hauseqcn.e	$⊢ φ \to {F ↾}_{A} = {G ↾}_{A}$
6		hauseqcn.a	$⊢ φ \to A \subseteq X$
7		hauseqcn.c	$⊢ φ \to cls (J) (A) = X$
8		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
9	3 8	syl	$⊢ φ \to J \in Top$
10		dmin	$⊢ dom (F \cap G) \subseteq dom F \cap dom G$
11		eqid	$⊢ ⋃ J = ⋃ J$
12		eqid	$⊢ ⋃ K = ⋃ K$
13	11 12	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
14		fdm	$⊢ F : ⋃ J ⟶ ⋃ K \to dom F = ⋃ J$
15	3 13 14	3syl	$⊢ φ \to dom F = ⋃ J$
16	11 12	cnf	$⊢ G \in (J Cn K) \to G : ⋃ J ⟶ ⋃ K$
17		fdm	$⊢ G : ⋃ J ⟶ ⋃ K \to dom G = ⋃ J$
18	4 16 17	3syl	$⊢ φ \to dom G = ⋃ J$
19	15 18	ineq12d	$⊢ φ \to dom F \cap dom G = ⋃ J \cap ⋃ J$
20		inidm	$⊢ ⋃ J \cap ⋃ J = ⋃ J$
21	19 20	syl6eq	$⊢ φ \to dom F \cap dom G = ⋃ J$
22	10 21	sseqtrid	$⊢ φ \to dom (F \cap G) \subseteq ⋃ J$
23		ffn	$⊢ F : ⋃ J ⟶ ⋃ K \to F Fn ⋃ J$
24	3 13 23	3syl	$⊢ φ \to F Fn ⋃ J$
25		ffn	$⊢ G : ⋃ J ⟶ ⋃ K \to G Fn ⋃ J$
26	4 16 25	3syl	$⊢ φ \to G Fn ⋃ J$
27	6 1	sseqtrdi	$⊢ φ \to A \subseteq ⋃ J$
28		fnreseql	$⊢ (F Fn ⋃ J \land G Fn ⋃ J \land A \subseteq ⋃ J) \to ({F ↾}_{A} = {G ↾}_{A} \leftrightarrow A \subseteq dom (F \cap G))$
29	24 26 27 28	syl3anc	$⊢ φ \to ({F ↾}_{A} = {G ↾}_{A} \leftrightarrow A \subseteq dom (F \cap G))$
30	5 29	mpbid	$⊢ φ \to A \subseteq dom (F \cap G)$
31	11	clsss	$⊢ (J \in Top \land dom (F \cap G) \subseteq ⋃ J \land A \subseteq dom (F \cap G)) \to cls (J) (A) \subseteq cls (J) (dom (F \cap G))$
32	9 22 30 31	syl3anc	$⊢ φ \to cls (J) (A) \subseteq cls (J) (dom (F \cap G))$
33	2 3 4	hauseqlcld	$⊢ φ \to dom (F \cap G) \in Clsd (J)$
34		cldcls	$⊢ dom (F \cap G) \in Clsd (J) \to cls (J) (dom (F \cap G)) = dom (F \cap G)$
35	33 34	syl	$⊢ φ \to cls (J) (dom (F \cap G)) = dom (F \cap G)$
36	32 7 35	3sstr3d	$⊢ φ \to X \subseteq dom (F \cap G)$
37	1 36	eqsstrrid	$⊢ φ \to ⋃ J \subseteq dom (F \cap G)$
38		fneqeql2	$⊢ (F Fn ⋃ J \land G Fn ⋃ J) \to (F = G \leftrightarrow ⋃ J \subseteq dom (F \cap G))$
39	24 26 38	syl2anc	$⊢ φ \to (F = G \leftrightarrow ⋃ J \subseteq dom (F \cap G))$
40	37 39	mpbird	$⊢ φ \to F = G$

Metamath Proof Explorer

Theorem hauseqcn

Proof