xkopjcn

Description: Continuity of a projection map from the space of continuous functions. (This theorem can be strengthened, to joint continuity in both f and A as a function on ( S ^ko R ) tX R , but not without stronger assumptions on R ; see xkofvcn .) (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Hypothesis	xkopjcn.1	$⊢ X = ⋃ R$
	Assertion	xkopjcn	$⊢ (R \in Top \land S \in Top \land A \in X) \to (f \in (R Cn S) ⟼ f (A)) \in ((S^_{ko} R) Cn S)$

Proof

Step	Hyp	Ref	Expression
1		xkopjcn.1	$⊢ X = ⋃ R$
2		eqid	$⊢ S^_{ko} R = S^_{ko} R$
3	2	xkotopon	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in TopOn (R Cn S)$
4	3	3adant3	$⊢ (R \in Top \land S \in Top \land A \in X) \to S^_{ko} R \in TopOn (R Cn S)$
5	1	topopn	$⊢ R \in Top \to X \in R$
6	5	3ad2ant1	$⊢ (R \in Top \land S \in Top \land A \in X) \to X \in R$
7		fconst6g	$⊢ S \in Top \to (X \times \{S\}) : X ⟶ Top$
8	7	3ad2ant2	$⊢ (R \in Top \land S \in Top \land A \in X) \to (X \times \{S\}) : X ⟶ Top$
9		pttop	$⊢ (X \in R \land (X \times \{S\}) : X ⟶ Top) \to \prod_{𝑡} (X \times \{S\}) \in Top$
10	6 8 9	syl2anc	$⊢ (R \in Top \land S \in Top \land A \in X) \to \prod_{𝑡} (X \times \{S\}) \in Top$
11		eqid	$⊢ ⋃ S = ⋃ S$
12	1 11	cnf	$⊢ f \in (R Cn S) \to f : X ⟶ ⋃ S$
13		uniexg	$⊢ S \in Top \to ⋃ S \in V$
14	13	3ad2ant2	$⊢ (R \in Top \land S \in Top \land A \in X) \to ⋃ S \in V$
15	14 6	elmapd	$⊢ (R \in Top \land S \in Top \land A \in X) \to (f \in ({⋃ S}^{X}) \leftrightarrow f : X ⟶ ⋃ S)$
16	12 15	syl5ibr	$⊢ (R \in Top \land S \in Top \land A \in X) \to (f \in (R Cn S) \to f \in ({⋃ S}^{X}))$
17	16	ssrdv	$⊢ (R \in Top \land S \in Top \land A \in X) \to R Cn S \subseteq {⋃ S}^{X}$
18		simp2	$⊢ (R \in Top \land S \in Top \land A \in X) \to S \in Top$
19		eqid	$⊢ \prod_{𝑡} (X \times \{S\}) = \prod_{𝑡} (X \times \{S\})$
20	19 11	ptuniconst	$⊢ (X \in R \land S \in Top) \to {⋃ S}^{X} = ⋃ \prod_{𝑡} (X \times \{S\})$
21	6 18 20	syl2anc	$⊢ (R \in Top \land S \in Top \land A \in X) \to {⋃ S}^{X} = ⋃ \prod_{𝑡} (X \times \{S\})$
22	17 21	sseqtrd	$⊢ (R \in Top \land S \in Top \land A \in X) \to R Cn S \subseteq ⋃ \prod_{𝑡} (X \times \{S\})$
23		eqid	$⊢ ⋃ \prod_{𝑡} (X \times \{S\}) = ⋃ \prod_{𝑡} (X \times \{S\})$
24	23	restuni	$⊢ (\prod_{𝑡} (X \times \{S\}) \in Top \land R Cn S \subseteq ⋃ \prod_{𝑡} (X \times \{S\})) \to R Cn S = ⋃ (\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S))$
25	10 22 24	syl2anc	$⊢ (R \in Top \land S \in Top \land A \in X) \to R Cn S = ⋃ (\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S))$
26	25	fveq2d	$⊢ (R \in Top \land S \in Top \land A \in X) \to TopOn (R Cn S) = TopOn (⋃ (\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S)))$
27	4 26	eleqtrd	$⊢ (R \in Top \land S \in Top \land A \in X) \to S^_{ko} R \in TopOn (⋃ (\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S)))$
28	1 19	xkoptsub	$⊢ (R \in Top \land S \in Top) \to \prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S) \subseteq S^_{ko} R$
29	28	3adant3	$⊢ (R \in Top \land S \in Top \land A \in X) \to \prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S) \subseteq S^_{ko} R$
30		eqid	$⊢ ⋃ (\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S)) = ⋃ (\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S))$
31	30	cnss1	$⊢ (S^_{ko} R \in TopOn (⋃ (\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S))) \land \prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S) \subseteq S^_{ko} R) \to (\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S)) Cn S \subseteq (S^_{ko} R) Cn S$
32	27 29 31	syl2anc	$⊢ (R \in Top \land S \in Top \land A \in X) \to (\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S)) Cn S \subseteq (S^_{ko} R) Cn S$
33	22	resmptd	$⊢ (R \in Top \land S \in Top \land A \in X) \to {(f \in ⋃ \prod_{𝑡} (X \times \{S\}) ⟼ f (A)) ↾}_{(R Cn S)} = (f \in (R Cn S) ⟼ f (A))$
34		simp3	$⊢ (R \in Top \land S \in Top \land A \in X) \to A \in X$
35	23 19	ptpjcn	$⊢ (X \in R \land (X \times \{S\}) : X ⟶ Top \land A \in X) \to (f \in ⋃ \prod_{𝑡} (X \times \{S\}) ⟼ f (A)) \in (\prod_{𝑡} (X \times \{S\}) Cn (X \times \{S\}) (A))$
36	6 8 34 35	syl3anc	$⊢ (R \in Top \land S \in Top \land A \in X) \to (f \in ⋃ \prod_{𝑡} (X \times \{S\}) ⟼ f (A)) \in (\prod_{𝑡} (X \times \{S\}) Cn (X \times \{S\}) (A))$
37		fvconst2g	$⊢ (S \in Top \land A \in X) \to (X \times \{S\}) (A) = S$
38	37	3adant1	$⊢ (R \in Top \land S \in Top \land A \in X) \to (X \times \{S\}) (A) = S$
39	38	oveq2d	$⊢ (R \in Top \land S \in Top \land A \in X) \to \prod_{𝑡} (X \times \{S\}) Cn (X \times \{S\}) (A) = \prod_{𝑡} (X \times \{S\}) Cn S$
40	36 39	eleqtrd	$⊢ (R \in Top \land S \in Top \land A \in X) \to (f \in ⋃ \prod_{𝑡} (X \times \{S\}) ⟼ f (A)) \in (\prod_{𝑡} (X \times \{S\}) Cn S)$
41	23	cnrest	$⊢ ((f \in ⋃ \prod_{𝑡} (X \times \{S\}) ⟼ f (A)) \in (\prod_{𝑡} (X \times \{S\}) Cn S) \land R Cn S \subseteq ⋃ \prod_{𝑡} (X \times \{S\})) \to {(f \in ⋃ \prod_{𝑡} (X \times \{S\}) ⟼ f (A)) ↾}_{(R Cn S)} \in ((\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S)) Cn S)$
42	40 22 41	syl2anc	$⊢ (R \in Top \land S \in Top \land A \in X) \to {(f \in ⋃ \prod_{𝑡} (X \times \{S\}) ⟼ f (A)) ↾}_{(R Cn S)} \in ((\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S)) Cn S)$
43	33 42	eqeltrrd	$⊢ (R \in Top \land S \in Top \land A \in X) \to (f \in (R Cn S) ⟼ f (A)) \in ((\prod_{𝑡} (X \times \{S\}) ↾_{𝑡} (R Cn S)) Cn S)$
44	32 43	sseldd	$⊢ (R \in Top \land S \in Top \land A \in X) \to (f \in (R Cn S) ⟼ f (A)) \in ((S^_{ko} R) Cn S)$

Metamath Proof Explorer

Theorem xkopjcn

Proof