xkoco2cn

Description: If F is a continuous function, then g |-> F o. g is a continuous function on function spaces. (Contributed by Mario Carneiro, 23-Mar-2015)

	Ref	Expression
Hypotheses	xkoco2cn.r	$⊢ φ \to R \in Top$
	xkoco2cn.f	$⊢ φ \to F \in (S Cn T)$
Assertion	xkoco2cn	$⊢ φ \to (g \in (R Cn S) ⟼ F \circ g) \in ((S^_{ko} R) Cn (T^_{ko} R))$

Proof

Step	Hyp	Ref	Expression
1		xkoco2cn.r	$⊢ φ \to R \in Top$
2		xkoco2cn.f	$⊢ φ \to F \in (S Cn T)$
3		simpr	$⊢ (φ \land g \in (R Cn S)) \to g \in (R Cn S)$
4	2	adantr	$⊢ (φ \land g \in (R Cn S)) \to F \in (S Cn T)$
5		cnco	$⊢ (g \in (R Cn S) \land F \in (S Cn T)) \to F \circ g \in (R Cn T)$
6	3 4 5	syl2anc	$⊢ (φ \land g \in (R Cn S)) \to F \circ g \in (R Cn T)$
7	6	fmpttd	$⊢ φ \to (g \in (R Cn S) ⟼ F \circ g) : R Cn S ⟶ R Cn T$
8		eqid	$⊢ ⋃ R = ⋃ R$
9		eqid	$⊢ \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} = \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}$
10		eqid	$⊢ (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) = (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\})$
11	8 9 10	xkobval	$⊢ ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) = \{x \| \exists k \in 𝒫 ⋃ R \exists v \in T (R ↾_{𝑡} k \in Comp \land x = \{h \in (R Cn T) \| h [k] \subseteq v\})\}$
12	11	abeq2i	$⊢ x \in ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) \leftrightarrow \exists k \in 𝒫 ⋃ R \exists v \in T (R ↾_{𝑡} k \in Comp \land x = \{h \in (R Cn T) \| h [k] \subseteq v\})$
13		simpr	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to g \in (R Cn S)$
14	2	ad3antrrr	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to F \in (S Cn T)$
15	13 14 5	syl2anc	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to F \circ g \in (R Cn T)$
16		imaeq1	$⊢ h = F \circ g \to h [k] = (F \circ g) [k]$
17		imaco	$⊢ (F \circ g) [k] = F [g [k]]$
18	16 17	eqtrdi	$⊢ h = F \circ g \to h [k] = F [g [k]]$
19	18	sseq1d	$⊢ h = F \circ g \to (h [k] \subseteq v \leftrightarrow F [g [k]] \subseteq v)$
20	19	elrab3	$⊢ F \circ g \in (R Cn T) \to (F \circ g \in \{h \in (R Cn T) \| h [k] \subseteq v\} \leftrightarrow F [g [k]] \subseteq v)$
21	15 20	syl	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to (F \circ g \in \{h \in (R Cn T) \| h [k] \subseteq v\} \leftrightarrow F [g [k]] \subseteq v)$
22		eqid	$⊢ ⋃ S = ⋃ S$
23		eqid	$⊢ ⋃ T = ⋃ T$
24	22 23	cnf	$⊢ F \in (S Cn T) \to F : ⋃ S ⟶ ⋃ T$
25	2 24	syl	$⊢ φ \to F : ⋃ S ⟶ ⋃ T$
26	25	ad3antrrr	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to F : ⋃ S ⟶ ⋃ T$
27	26	ffund	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to Fun F$
28		imassrn	$⊢ g [k] \subseteq ran g$
29	8 22	cnf	$⊢ g \in (R Cn S) \to g : ⋃ R ⟶ ⋃ S$
30	13 29	syl	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to g : ⋃ R ⟶ ⋃ S$
31	30	frnd	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to ran g \subseteq ⋃ S$
32	28 31	sstrid	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to g [k] \subseteq ⋃ S$
33	26	fdmd	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to dom F = ⋃ S$
34	32 33	sseqtrrd	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to g [k] \subseteq dom F$
35		funimass3	$⊢ (Fun F \land g [k] \subseteq dom F) \to (F [g [k]] \subseteq v \leftrightarrow g [k] \subseteq F^{-1} [v])$
36	27 34 35	syl2anc	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to (F [g [k]] \subseteq v \leftrightarrow g [k] \subseteq F^{-1} [v])$
37	21 36	bitrd	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (R Cn S)) \to (F \circ g \in \{h \in (R Cn T) \| h [k] \subseteq v\} \leftrightarrow g [k] \subseteq F^{-1} [v])$
38	37	rabbidva	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to \{g \in (R Cn S) \| F \circ g \in \{h \in (R Cn T) \| h [k] \subseteq v\}\} = \{g \in (R Cn S) \| g [k] \subseteq F^{-1} [v]\}$
39	1	ad2antrr	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to R \in Top$
40		cntop1	$⊢ F \in (S Cn T) \to S \in Top$
41	2 40	syl	$⊢ φ \to S \in Top$
42	41	ad2antrr	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to S \in Top$
43		simplrl	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to k \in 𝒫 ⋃ R$
44	43	elpwid	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to k \subseteq ⋃ R$
45		simpr	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to R ↾_{𝑡} k \in Comp$
46	2	ad2antrr	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to F \in (S Cn T)$
47		simplrr	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to v \in T$
48		cnima	$⊢ (F \in (S Cn T) \land v \in T) \to F^{-1} [v] \in S$
49	46 47 48	syl2anc	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to F^{-1} [v] \in S$
50	8 39 42 44 45 49	xkoopn	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to \{g \in (R Cn S) \| g [k] \subseteq F^{-1} [v]\} \in (S^_{ko} R)$
51	38 50	eqeltrd	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to \{g \in (R Cn S) \| F \circ g \in \{h \in (R Cn T) \| h [k] \subseteq v\}\} \in (S^_{ko} R)$
52		imaeq2	$⊢ x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [x] = {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]$
53		eqid	$⊢ (g \in (R Cn S) ⟼ F \circ g) = (g \in (R Cn S) ⟼ F \circ g)$
54	53	mptpreima	$⊢ {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] = \{g \in (R Cn S) \| F \circ g \in \{h \in (R Cn T) \| h [k] \subseteq v\}\}$
55	52 54	eqtrdi	$⊢ x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [x] = \{g \in (R Cn S) \| F \circ g \in \{h \in (R Cn T) \| h [k] \subseteq v\}\}$
56	55	eleq1d	$⊢ x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to ({(g \in (R Cn S) ⟼ F \circ g)}^{-1} [x] \in (S^_{ko} R) \leftrightarrow \{g \in (R Cn S) \| F \circ g \in \{h \in (R Cn T) \| h [k] \subseteq v\}\} \in (S^_{ko} R))$
57	51 56	syl5ibrcom	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to (x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [x] \in (S^_{ko} R))$
58	57	expimpd	$⊢ (φ \land (k \in 𝒫 ⋃ R \land v \in T)) \to ((R ↾_{𝑡} k \in Comp \land x = \{h \in (R Cn T) \| h [k] \subseteq v\}) \to {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [x] \in (S^_{ko} R))$
59	58	rexlimdvva	$⊢ φ \to (\exists k \in 𝒫 ⋃ R \exists v \in T (R ↾_{𝑡} k \in Comp \land x = \{h \in (R Cn T) \| h [k] \subseteq v\}) \to {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [x] \in (S^_{ko} R))$
60	12 59	syl5bi	$⊢ φ \to (x \in ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) \to {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [x] \in (S^_{ko} R))$
61	60	ralrimiv	$⊢ φ \to \forall x \in ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [x] \in (S^_{ko} R)$
62		eqid	$⊢ S^_{ko} R = S^_{ko} R$
63	62	xkotopon	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in TopOn (R Cn S)$
64	1 41 63	syl2anc	$⊢ φ \to S^_{ko} R \in TopOn (R Cn S)$
65		ovex	$⊢ R Cn T \in V$
66	65	pwex	$⊢ 𝒫 (R Cn T) \in V$
67	8 9 10	xkotf	$⊢ (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) : \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} \times T ⟶ 𝒫 (R Cn T)$
68		frn	$⊢ (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) : \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} \times T ⟶ 𝒫 (R Cn T) \to ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) \subseteq 𝒫 (R Cn T)$
69	67 68	ax-mp	$⊢ ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) \subseteq 𝒫 (R Cn T)$
70	66 69	ssexi	$⊢ ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) \in V$
71	70	a1i	$⊢ φ \to ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) \in V$
72		cntop2	$⊢ F \in (S Cn T) \to T \in Top$
73	2 72	syl	$⊢ φ \to T \in Top$
74	8 9 10	xkoval	$⊢ (R \in Top \land T \in Top) \to T^_{ko} R = topGen (fi (ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\})))$
75	1 73 74	syl2anc	$⊢ φ \to T^_{ko} R = topGen (fi (ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\})))$
76		eqid	$⊢ T^_{ko} R = T^_{ko} R$
77	76	xkotopon	$⊢ (R \in Top \land T \in Top) \to T^_{ko} R \in TopOn (R Cn T)$
78	1 73 77	syl2anc	$⊢ φ \to T^_{ko} R \in TopOn (R Cn T)$
79	64 71 75 78	subbascn	$⊢ φ \to ((g \in (R Cn S) ⟼ F \circ g) \in ((S^_{ko} R) Cn (T^_{ko} R)) \leftrightarrow ((g \in (R Cn S) ⟼ F \circ g) : R Cn S ⟶ R Cn T \land \forall x \in ran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) {(g \in (R Cn S) ⟼ F \circ g)}^{-1} [x] \in (S^_{ko} R)))$
80	7 61 79	mpbir2and	$⊢ φ \to (g \in (R Cn S) ⟼ F \circ g) \in ((S^_{ko} R) Cn (T^_{ko} R))$

Metamath Proof Explorer

Theorem xkoco2cn

Proof