xkoco1cn

Description: If F is a continuous function, then g |-> g o. F is a continuous function on function spaces. (The reason we prove this and xkoco2cn independently of the more general xkococn is because that requires some inconvenient extra assumptions on S .) (Contributed by Mario Carneiro, 20-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		xkoco1cn.t	$⊢ φ \to T \in Top$
2		xkoco1cn.f	$⊢ φ \to F \in (R Cn S)$
3		cnco	$⊢ (F \in (R Cn S) \land g \in (S Cn T)) \to g \circ F \in (R Cn T)$
4	2 3	sylan	$⊢ (φ \land g \in (S Cn T)) \to g \circ F \in (R Cn T)$
5	4	fmpttd	$⊢ φ \to (g \in (S Cn T) ⟼ g \circ F) : S Cn T ⟶ R Cn T$
6		eqid	$⊢ ⋃ R = ⋃ R$
7		eqid	$⊢ \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} = \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}$
8		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\})$
9	6 7 8	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\})\}$
10	9	eqabri	$⊢ 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\})$
11	2	ad2antrr	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to F \in (R Cn S)$
12	11 3	sylan	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (S Cn T)) \to g \circ F \in (R Cn T)$
13		imaeq1	$⊢ h = g \circ F \to h [k] = (g \circ F) [k]$
14		imaco	$⊢ (g \circ F) [k] = g [F [k]]$
15	13 14	eqtrdi	$⊢ h = g \circ F \to h [k] = g [F [k]]$
16	15	sseq1d	$⊢ h = g \circ F \to (h [k] \subseteq v \leftrightarrow g [F [k]] \subseteq v)$
17	16	elrab3	$⊢ g \circ F \in (R Cn T) \to (g \circ F \in \{h \in (R Cn T) \| h [k] \subseteq v\} \leftrightarrow g [F [k]] \subseteq v)$
18	12 17	syl	$⊢ (((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \land g \in (S Cn T)) \to (g \circ F \in \{h \in (R Cn T) \| h [k] \subseteq v\} \leftrightarrow g [F [k]] \subseteq v)$
19	18	rabbidva	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to \{g \in (S Cn T) \| g \circ F \in \{h \in (R Cn T) \| h [k] \subseteq v\}\} = \{g \in (S Cn T) \| g [F [k]] \subseteq v\}$
20		eqid	$⊢ ⋃ S = ⋃ S$
21		cntop2	$⊢ F \in (R Cn S) \to S \in Top$
22	2 21	syl	$⊢ φ \to S \in Top$
23	22	ad2antrr	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to S \in Top$
24	1	ad2antrr	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to T \in Top$
25		imassrn	$⊢ F [k] \subseteq ran F$
26	6 20	cnf	$⊢ F \in (R Cn S) \to F : ⋃ R ⟶ ⋃ S$
27		frn	$⊢ F : ⋃ R ⟶ ⋃ S \to ran F \subseteq ⋃ S$
28	11 26 27	3syl	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to ran F \subseteq ⋃ S$
29	25 28	sstrid	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to F [k] \subseteq ⋃ S$
30		imacmp	$⊢ (F \in (R Cn S) \land R ↾_{𝑡} k \in Comp) \to S ↾_{𝑡} F [k] \in Comp$
31	11 30	sylancom	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to S ↾_{𝑡} F [k] \in Comp$
32		simplrr	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to v \in T$
33	20 23 24 29 31 32	xkoopn	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to \{g \in (S Cn T) \| g [F [k]] \subseteq v\} \in (T^_{ko} S)$
34	19 33	eqeltrd	$⊢ ((φ \land (k \in 𝒫 ⋃ R \land v \in T)) \land R ↾_{𝑡} k \in Comp) \to \{g \in (S Cn T) \| g \circ F \in \{h \in (R Cn T) \| h [k] \subseteq v\}\} \in (T^_{ko} S)$
35		imaeq2	$⊢ x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to {(g \in (S Cn T) ⟼ g \circ F)}^{-1} [x] = {(g \in (S Cn T) ⟼ g \circ F)}^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]$
36		eqid	$⊢ (g \in (S Cn T) ⟼ g \circ F) = (g \in (S Cn T) ⟼ g \circ F)$
37	36	mptpreima	$⊢ {(g \in (S Cn T) ⟼ g \circ F)}^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] = \{g \in (S Cn T) \| g \circ F \in \{h \in (R Cn T) \| h [k] \subseteq v\}\}$
38	35 37	eqtrdi	$⊢ x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to {(g \in (S Cn T) ⟼ g \circ F)}^{-1} [x] = \{g \in (S Cn T) \| g \circ F \in \{h \in (R Cn T) \| h [k] \subseteq v\}\}$
39	38	eleq1d	$⊢ x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to ({(g \in (S Cn T) ⟼ g \circ F)}^{-1} [x] \in (T^_{ko} S) \leftrightarrow \{g \in (S Cn T) \| g \circ F \in \{h \in (R Cn T) \| h [k] \subseteq v\}\} \in (T^_{ko} S))$
40	34 39	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 (S Cn T) ⟼ g \circ F)}^{-1} [x] \in (T^_{ko} S))$
41	40	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 (S Cn T) ⟼ g \circ F)}^{-1} [x] \in (T^_{ko} S))$
42	41	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 (S Cn T) ⟼ g \circ F)}^{-1} [x] \in (T^_{ko} S))$
43	10 42	biimtrid	$⊢ φ \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 (S Cn T) ⟼ g \circ F)}^{-1} [x] \in (T^_{ko} S))$
44	43	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 (S Cn T) ⟼ g \circ F)}^{-1} [x] \in (T^_{ko} S)$
45		eqid	$⊢ T^_{ko} S = T^_{ko} S$
46	45	xkotopon	$⊢ (S \in Top \land T \in Top) \to T^_{ko} S \in TopOn (S Cn T)$
47	22 1 46	syl2anc	$⊢ φ \to T^_{ko} S \in TopOn (S Cn T)$
48		ovex	$⊢ R Cn T \in V$
49	48	pwex	$⊢ 𝒫 (R Cn T) \in V$
50	6 7 8	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)$
51		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)$
52	50 51	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)$
53	49 52	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$
54	53	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$
55		cntop1	$⊢ F \in (R Cn S) \to R \in Top$
56	2 55	syl	$⊢ φ \to R \in Top$
57	6 7 8	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\})))$
58	56 1 57	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\})))$
59		eqid	$⊢ T^_{ko} R = T^_{ko} R$
60	59	xkotopon	$⊢ (R \in Top \land T \in Top) \to T^_{ko} R \in TopOn (R Cn T)$
61	56 1 60	syl2anc	$⊢ φ \to T^_{ko} R \in TopOn (R Cn T)$
62	47 54 58 61	subbascn	$⊢ φ \to ((g \in (S Cn T) ⟼ g \circ F) \in ((T^_{ko} S) Cn (T^_{ko} R)) \leftrightarrow ((g \in (S Cn T) ⟼ g \circ F) : S Cn T ⟶ 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 (S Cn T) ⟼ g \circ F)}^{-1} [x] \in (T^_{ko} S)))$
63	5 44 62	mpbir2and	$⊢ φ \to (g \in (S Cn T) ⟼ g \circ F) \in ((T^_{ko} S) Cn (T^_{ko} R))$

Metamath Proof Explorer

Theorem xkoco1cn

Proof