cnconst2

Description: A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Assertion	cnconst2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \to X \times \{B\} \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		fconst6g	$⊢ B \in Y \to (X \times \{B\}) : X ⟶ Y$
2	1	3ad2ant3	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \to (X \times \{B\}) : X ⟶ Y$
3	2	adantr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \to (X \times \{B\}) : X ⟶ Y$
4		simpll3	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land y \in K) \to B \in Y$
5		simplr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land y \in K) \to x \in X$
6		fvconst2g	$⊢ (B \in Y \land x \in X) \to (X \times \{B\}) (x) = B$
7	4 5 6	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land y \in K) \to (X \times \{B\}) (x) = B$
8	7	eleq1d	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land y \in K) \to ((X \times \{B\}) (x) \in y \leftrightarrow B \in y)$
9		simpll1	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land (y \in K \land B \in y)) \to J \in TopOn (X)$
10		toponmax	$⊢ J \in TopOn (X) \to X \in J$
11	9 10	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land (y \in K \land B \in y)) \to X \in J$
12		simplr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land (y \in K \land B \in y)) \to x \in X$
13		df-ima	$⊢ (X \times \{B\}) [X] = ran ({(X \times \{B\}) ↾}_{X})$
14		ssid	$⊢ X \subseteq X$
15		xpssres	$⊢ X \subseteq X \to {(X \times \{B\}) ↾}_{X} = X \times \{B\}$
16	14 15	ax-mp	$⊢ {(X \times \{B\}) ↾}_{X} = X \times \{B\}$
17	16	rneqi	$⊢ ran ({(X \times \{B\}) ↾}_{X}) = ran (X \times \{B\})$
18		rnxpss	$⊢ ran (X \times \{B\}) \subseteq \{B\}$
19	17 18	eqsstri	$⊢ ran ({(X \times \{B\}) ↾}_{X}) \subseteq \{B\}$
20		simprr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land (y \in K \land B \in y)) \to B \in y$
21	20	snssd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land (y \in K \land B \in y)) \to \{B\} \subseteq y$
22	19 21	sstrid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land (y \in K \land B \in y)) \to ran ({(X \times \{B\}) ↾}_{X}) \subseteq y$
23	13 22	eqsstrid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land (y \in K \land B \in y)) \to (X \times \{B\}) [X] \subseteq y$
24		eleq2	$⊢ u = X \to (x \in u \leftrightarrow x \in X)$
25		imaeq2	$⊢ u = X \to (X \times \{B\}) [u] = (X \times \{B\}) [X]$
26	25	sseq1d	$⊢ u = X \to ((X \times \{B\}) [u] \subseteq y \leftrightarrow (X \times \{B\}) [X] \subseteq y)$
27	24 26	anbi12d	$⊢ u = X \to ((x \in u \land (X \times \{B\}) [u] \subseteq y) \leftrightarrow (x \in X \land (X \times \{B\}) [X] \subseteq y))$
28	27	rspcev	$⊢ (X \in J \land (x \in X \land (X \times \{B\}) [X] \subseteq y)) \to \exists u \in J (x \in u \land (X \times \{B\}) [u] \subseteq y)$
29	11 12 23 28	syl12anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land (y \in K \land B \in y)) \to \exists u \in J (x \in u \land (X \times \{B\}) [u] \subseteq y)$
30	29	expr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land y \in K) \to (B \in y \to \exists u \in J (x \in u \land (X \times \{B\}) [u] \subseteq y))$
31	8 30	sylbid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \land y \in K) \to ((X \times \{B\}) (x) \in y \to \exists u \in J (x \in u \land (X \times \{B\}) [u] \subseteq y))$
32	31	ralrimiva	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \to \forall y \in K ((X \times \{B\}) (x) \in y \to \exists u \in J (x \in u \land (X \times \{B\}) [u] \subseteq y))$
33		simpl1	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \to J \in TopOn (X)$
34		simpl2	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \to K \in TopOn (Y)$
35		simpr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \to x \in X$
36		iscnp	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land x \in X) \to (X \times \{B\} \in (J CnP K) (x) \leftrightarrow ((X \times \{B\}) : X ⟶ Y \land \forall y \in K ((X \times \{B\}) (x) \in y \to \exists u \in J (x \in u \land (X \times \{B\}) [u] \subseteq y))))$
37	33 34 35 36	syl3anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \to (X \times \{B\} \in (J CnP K) (x) \leftrightarrow ((X \times \{B\}) : X ⟶ Y \land \forall y \in K ((X \times \{B\}) (x) \in y \to \exists u \in J (x \in u \land (X \times \{B\}) [u] \subseteq y))))$
38	3 32 37	mpbir2and	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \land x \in X) \to X \times \{B\} \in (J CnP K) (x)$
39	38	ralrimiva	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \to \forall x \in X X \times \{B\} \in (J CnP K) (x)$
40		cncnp	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (X \times \{B\} \in (J Cn K) \leftrightarrow ((X \times \{B\}) : X ⟶ Y \land \forall x \in X X \times \{B\} \in (J CnP K) (x)))$
41	40	3adant3	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \to (X \times \{B\} \in (J Cn K) \leftrightarrow ((X \times \{B\}) : X ⟶ Y \land \forall x \in X X \times \{B\} \in (J CnP K) (x)))$
42	2 39 41	mpbir2and	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \to X \times \{B\} \in (J Cn K)$

Metamath Proof Explorer

Theorem cnconst2

Proof