dnsconst

Description: If a continuous mapping to a T_1 space is constant on a dense subset, it is constant on the entire space. Note that ( ( clsJ )A ) = X means " A is dense in X " and A C_ (`' F " { P } ) means " F is constant on A ` " (see funconstss ). (Contributed by NM, 15-Mar-2007) (Proof shortened by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	dnsconst.1	$⊢ X = ⋃ J$
	dnsconst.2	$⊢ Y = ⋃ K$
Assertion	dnsconst	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to F : X ⟶ \{P\}$

Proof

Step	Hyp	Ref	Expression
1		dnsconst.1	$⊢ X = ⋃ J$
2		dnsconst.2	$⊢ Y = ⋃ K$
3		simplr	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to F \in (J Cn K)$
4	1 2	cnf	$⊢ F \in (J Cn K) \to F : X ⟶ Y$
5		ffn	$⊢ F : X ⟶ Y \to F Fn X$
6	3 4 5	3syl	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to F Fn X$
7		simpr3	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to cls (J) (A) = X$
8		simpll	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to K \in Fre$
9		simpr1	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to P \in Y$
10	2	t1sncld	$⊢ (K \in Fre \land P \in Y) \to \{P\} \in Clsd (K)$
11	8 9 10	syl2anc	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to \{P\} \in Clsd (K)$
12		cnclima	$⊢ (F \in (J Cn K) \land \{P\} \in Clsd (K)) \to F^{-1} [\{P\}] \in Clsd (J)$
13	3 11 12	syl2anc	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to F^{-1} [\{P\}] \in Clsd (J)$
14		simpr2	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to A \subseteq F^{-1} [\{P\}]$
15	1	clsss2	$⊢ (F^{-1} [\{P\}] \in Clsd (J) \land A \subseteq F^{-1} [\{P\}]) \to cls (J) (A) \subseteq F^{-1} [\{P\}]$
16	13 14 15	syl2anc	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to cls (J) (A) \subseteq F^{-1} [\{P\}]$
17	7 16	eqsstrrd	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to X \subseteq F^{-1} [\{P\}]$
18		fconst3	$⊢ F : X ⟶ \{P\} \leftrightarrow (F Fn X \land X \subseteq F^{-1} [\{P\}])$
19	6 17 18	sylanbrc	$⊢ ((K \in Fre \land F \in (J Cn K)) \land (P \in Y \land A \subseteq F^{-1} [\{P\}] \land cls (J) (A) = X)) \to F : X ⟶ \{P\}$

Metamath Proof Explorer

Theorem dnsconst

Proof