xkococn

Description: Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Hypothesis	xkococn.1	$⊢ F = (f \in (S Cn T), g \in (R Cn S) ⟼ f \circ g)$
	Assertion	xkococn	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toF \in (((T^_{ko} S) \times_{t} (S^_{ko} R)) Cn (T^_{ko} R)))$

Proof

Step	Hyp	Ref	Expression
1		xkococn.1	$⊢ F = (f \in (S Cn T), g \in (R Cn S) ⟼ f \circ g)$
2		simprr	$⊢ ((R \in Top \land S \in N-LocallyComp\landT \in Top\land(f \in (S Cn T) \land g \in (R Cn S))\tog \in (R Cn S)))$
3		simprl	$⊢ ((R \in Top \land S \in N-LocallyComp\landT \in Top\land(f \in (S Cn T) \land g \in (R Cn S))\tof \in (S Cn T)))$
4		cnco	$⊢ (g \in (R Cn S) \land f \in (S Cn T)) \to f \circ g \in (R Cn T)$
5	2 3 4	syl2anc	$⊢ ((R \in Top \land S \in N-LocallyComp\landT \in Top\land(f \in (S Cn T) \land g \in (R Cn S))\tof \circ g \in (R Cn T)))$
6	5	ralrimivva	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\to\forall f \in (S Cn T) \forall g \in (R Cn S) f \circ g \in (R Cn T))$
7	1	fmpo	$⊢ \forall f \in (S Cn T) \forall g \in (R Cn S) f \circ g \in (R Cn T) \leftrightarrow F : (S Cn T) \times (R Cn S) ⟶ R Cn T$
8	6 7	sylib	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toF : (S Cn T) \times (R Cn S) ⟶ R Cn T)$
9		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\})$
10	9	rnmpo	$⊢ 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 \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} \exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\}\}$
11	10	eleq2i	$⊢ 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 x \in \{x \| \exists k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} \exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\}\}$
12		abid	$⊢ x \in \{x \| \exists k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} \exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\}\} \leftrightarrow \exists k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} \exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\}$
13		oveq2	$⊢ y = k \to R ↾_{𝑡} y = R ↾_{𝑡} k$
14	13	eleq1d	$⊢ y = k \to (R ↾_{𝑡} y \in Comp \leftrightarrow R ↾_{𝑡} k \in Comp)$
15	14	rexrab	$⊢ \exists k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} \exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\} \leftrightarrow \exists k \in 𝒫 ⋃ R (R ↾_{𝑡} k \in Comp \land \exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\})$
16	11 12 15	3bitri	$⊢ 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 (R ↾_{𝑡} k \in Comp \land \exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\})$
17	8	ad2antrr	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\toF : (S Cn T) \times (R Cn S) ⟶ R Cn T)))$
18		ffn	$⊢ F : (S Cn T) \times (R Cn S) ⟶ R Cn T \to F Fn ((S Cn T) \times (R Cn S))$
19		elpreima	$⊢ F Fn ((S Cn T) \times (R Cn S)) \to (y \in F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \leftrightarrow (y \in ((S Cn T) \times (R Cn S)) \land F (y) \in \{h \in (R Cn T) \| h [k] \subseteq v\}))$
20	17 18 19	3syl	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\to(y \in F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \leftrightarrow (y \in ((S Cn T) \times (R Cn S)) \land F (y) \in \{h \in (R Cn T) \| h [k] \subseteq v\})))))$
21		coeq1	$⊢ f = a \to f \circ g = a \circ g$
22		coeq2	$⊢ g = b \to a \circ g = a \circ b$
23		vex	$⊢ a \in V$
24		vex	$⊢ b \in V$
25	23 24	coex	$⊢ a \circ b \in V$
26	21 22 1 25	ovmpo	$⊢ (a \in (S Cn T) \land b \in (R Cn S)) \to a F b = a \circ b$
27	26	adantl	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land(a \in (S Cn T) \land b \in (R Cn S))\toa F b = a \circ b))))$
28	27	eleq1d	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land(a \in (S Cn T) \land b \in (R Cn S))\to(a F b \in \{h \in (R Cn T) \| h [k] \subseteq v\} \leftrightarrow a \circ b \in \{h \in (R Cn T) \| h [k] \subseteq v\})))))$
29		imaeq1	$⊢ h = a \circ b \to h [k] = (a \circ b) [k]$
30	29	sseq1d	$⊢ h = a \circ b \to (h [k] \subseteq v \leftrightarrow (a \circ b) [k] \subseteq v)$
31	30	elrab	$⊢ a \circ b \in \{h \in (R Cn T) \| h [k] \subseteq v\} \leftrightarrow (a \circ b \in (R Cn T) \land (a \circ b) [k] \subseteq v)$
32	31	simprbi	$⊢ a \circ b \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to (a \circ b) [k] \subseteq v$
33		simp2	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toS \in N-LocallyComp)$
34	33	ad3antrrr	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land((a \in (S Cn T) \land b \in (R Cn S)) \land (a \circ b) [k] \subseteq v)\toS \in N-LocallyComp))))$
35		elpwi	$⊢ k \in 𝒫 ⋃ R \to k \subseteq ⋃ R$
36	35	ad2antrl	$⊢ ((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\tok \subseteq ⋃ R))$
37	36	ad2antrr	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land((a \in (S Cn T) \land b \in (R Cn S)) \land (a \circ b) [k] \subseteq v)\tok \subseteq ⋃ R))))$
38		simprr	$⊢ ((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\toR ↾_{𝑡} k \in Comp))$
39	38	ad2antrr	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land((a \in (S Cn T) \land b \in (R Cn S)) \land (a \circ b) [k] \subseteq v)\toR ↾_{𝑡} k \in Comp))))$
40		simplr	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land((a \in (S Cn T) \land b \in (R Cn S)) \land (a \circ b) [k] \subseteq v)\tov \in T))))$
41		simprll	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land((a \in (S Cn T) \land b \in (R Cn S)) \land (a \circ b) [k] \subseteq v)\toa \in (S Cn T)))))$
42		simprlr	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land((a \in (S Cn T) \land b \in (R Cn S)) \land (a \circ b) [k] \subseteq v)\tob \in (R Cn S)))))$
43		simprr	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land((a \in (S Cn T) \land b \in (R Cn S)) \land (a \circ b) [k] \subseteq v)\to(a \circ b) [k] \subseteq v))))$
44	1 34 37 39 40 41 42 43	xkococnlem	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land((a \in (S Cn T) \land b \in (R Cn S)) \land (a \circ b) [k] \subseteq v)\to\exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨a, b⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}])))))$
45	44	expr	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land(a \in (S Cn T) \land b \in (R Cn S))\to((a \circ b) [k] \subseteq v \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨a, b⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]))))))$
46	32 45	syl5	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land(a \in (S Cn T) \land b \in (R Cn S))\to(a \circ b \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨a, b⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]))))))$
47	28 46	sylbid	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\land(a \in (S Cn T) \land b \in (R Cn S))\to(a F b \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨a, b⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]))))))$
48	47	ralrimivva	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\to\forall a \in (S Cn T) \forall b \in (R Cn S) (a F b \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨a, b⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}])))))$
49		fveq2	$⊢ y = ⟨a, b⟩ \to F (y) = F (⟨a, b⟩)$
50		df-ov	$⊢ a F b = F (⟨a, b⟩)$
51	49 50	eqtr4di	$⊢ y = ⟨a, b⟩ \to F (y) = a F b$
52	51	eleq1d	$⊢ y = ⟨a, b⟩ \to (F (y) \in \{h \in (R Cn T) \| h [k] \subseteq v\} \leftrightarrow a F b \in \{h \in (R Cn T) \| h [k] \subseteq v\})$
53		eleq1	$⊢ y = ⟨a, b⟩ \to (y \in z \leftrightarrow ⟨a, b⟩ \in z)$
54	53	anbi1d	$⊢ y = ⟨a, b⟩ \to ((y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]) \leftrightarrow (⟨a, b⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]))$
55	54	rexbidv	$⊢ y = ⟨a, b⟩ \to (\exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]) \leftrightarrow \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨a, b⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]))$
56	52 55	imbi12d	$⊢ y = ⟨a, b⟩ \to ((F (y) \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}])) \leftrightarrow (a F b \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨a, b⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}])))$
57	56	ralxp	$⊢ \forall y \in ((S Cn T) \times (R Cn S)) (F (y) \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}])) \leftrightarrow \forall a \in (S Cn T) \forall b \in (R Cn S) (a F b \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨a, b⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]))$
58	48 57	sylibr	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\to\forall y \in ((S Cn T) \times (R Cn S)) (F (y) \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}])))))$
59	58	r19.21bi	$⊢ ((((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\landy \in ((S Cn T) \times (R Cn S))\to(F (y) \in \{h \in (R Cn T) \| h [k] \subseteq v\} \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]))))))$
60	59	expimpd	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\to((y \in ((S Cn T) \times (R Cn S)) \land F (y) \in \{h \in (R Cn T) \| h [k] \subseteq v\}) \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}])))))$
61	20 60	sylbid	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\to(y \in F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}])))))$
62	61	ralrimiv	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\to\forall y \in F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]))))$
63		nllytop	$⊢ S \in N-LocallyComp\toS \in Top$
64	63	3ad2ant2	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toS \in Top)$
65		simp3	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toT \in Top)$
66		xkotop	$⊢ (S \in Top \land T \in Top) \to T^_{ko} S \in Top$
67	64 65 66	syl2anc	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toT^_{ko} S \in Top)$
68		simp1	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toR \in Top)$
69		xkotop	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in Top$
70	68 64 69	syl2anc	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toS^_{ko} R \in Top)$
71		txtop	$⊢ (T^_{ko} S \in Top \land S^_{ko} R \in Top) \to (T^_{ko} S) \times_{t} (S^_{ko} R) \in Top$
72	67 70 71	syl2anc	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\to(T^_{ko} S) \times_{t} (S^_{ko} R) \in Top)$
73	72	ad2antrr	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\to(T^_{ko} S) \times_{t} (S^_{ko} R) \in Top)))$
74		eltop2	$⊢ (T^_{ko} S) \times_{t} (S^_{ko} R) \in Top \to (F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) \leftrightarrow \forall y \in F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]))$
75	73 74	syl	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\to(F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) \leftrightarrow \forall y \in F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (y \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}])))))$
76	62 75	mpbird	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\toF^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \in ((T^_{ko} S) \times_{t} (S^_{ko} R)))))$
77		imaeq2	$⊢ x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to F^{-1} [x] = F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}]$
78	77	eleq1d	$⊢ x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to (F^{-1} [x] \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) \leftrightarrow F^{-1} [\{h \in (R Cn T) \| h [k] \subseteq v\}] \in ((T^_{ko} S) \times_{t} (S^_{ko} R)))$
79	76 78	syl5ibrcom	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\landv \in T\to(x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to F^{-1} [x] \in ((T^_{ko} S) \times_{t} (S^_{ko} R))))))$
80	79	rexlimdva	$⊢ ((R \in Top \land S \in N-LocallyComp\landT \in Top\land(k \in 𝒫 ⋃ R \land R ↾_{𝑡} k \in Comp)\to(\exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to F^{-1} [x] \in ((T^_{ko} S) \times_{t} (S^_{ko} R)))))$
81	80	anassrs	$⊢ (((R \in Top \land S \in N-LocallyComp\landT \in Top\landk \in 𝒫 ⋃ R\landR ↾_{𝑡} k \in Comp\to(\exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\} \to F^{-1} [x] \in ((T^_{ko} S) \times_{t} (S^_{ko} R))))))$
82	81	expimpd	$⊢ ((R \in Top \land S \in N-LocallyComp\landT \in Top\landk \in 𝒫 ⋃ R\to((R ↾_{𝑡} k \in Comp \land \exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\}) \to F^{-1} [x] \in ((T^_{ko} S) \times_{t} (S^_{ko} R)))))$
83	82	rexlimdva	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\to(\exists k \in 𝒫 ⋃ R (R ↾_{𝑡} k \in Comp \land \exists v \in T x = \{h \in (R Cn T) \| h [k] \subseteq v\}) \to F^{-1} [x] \in ((T^_{ko} S) \times_{t} (S^_{ko} R))))$
84	16 83	biimtrid	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\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 F^{-1} [x] \in ((T^_{ko} S) \times_{t} (S^_{ko} R))))$
85	84	ralrimiv	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\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\}) F^{-1} [x] \in ((T^_{ko} S) \times_{t} (S^_{ko} R)))$
86		eqid	$⊢ T^_{ko} S = T^_{ko} S$
87	86	xkotopon	$⊢ (S \in Top \land T \in Top) \to T^_{ko} S \in TopOn (S Cn T)$
88	64 65 87	syl2anc	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toT^_{ko} S \in TopOn (S Cn T))$
89		eqid	$⊢ S^_{ko} R = S^_{ko} R$
90	89	xkotopon	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in TopOn (R Cn S)$
91	68 64 90	syl2anc	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toS^_{ko} R \in TopOn (R Cn S))$
92		txtopon	$⊢ (T^_{ko} S \in TopOn (S Cn T) \land S^_{ko} R \in TopOn (R Cn S)) \to (T^_{ko} S) \times_{t} (S^_{ko} R) \in TopOn ((S Cn T) \times (R Cn S))$
93	88 91 92	syl2anc	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\to(T^_{ko} S) \times_{t} (S^_{ko} R) \in TopOn ((S Cn T) \times (R Cn S)))$
94		ovex	$⊢ R Cn T \in V$
95	94	pwex	$⊢ 𝒫 (R Cn T) \in V$
96		eqid	$⊢ ⋃ R = ⋃ R$
97		eqid	$⊢ \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\} = \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}$
98	96 97 9	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)$
99		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)$
100	98 99	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)$
101	95 100	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$
102	101	a1i	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toran (k \in \{y \in 𝒫 ⋃ R \| R ↾_{𝑡} y \in Comp\}, v \in T ⟼ \{h \in (R Cn T) \| h [k] \subseteq v\}) \in V)$
103	96 97 9	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\})))$
104	103	3adant2	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toT^_{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\}))))$
105		eqid	$⊢ T^_{ko} R = T^_{ko} R$
106	105	xkotopon	$⊢ (R \in Top \land T \in Top) \to T^_{ko} R \in TopOn (R Cn T)$
107	106	3adant2	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toT^_{ko} R \in TopOn (R Cn T))$
108	93 102 104 107	subbascn	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\to(F \in (((T^_{ko} S) \times_{t} (S^_{ko} R)) Cn (T^_{ko} R)) \leftrightarrow (F : (S Cn T) \times (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\}) F^{-1} [x] \in ((T^_{ko} S) \times_{t} (S^_{ko} R)))))$
109	8 85 108	mpbir2and	$⊢ (R \in Top \land S \in N-LocallyComp\landT \in Top\toF \in (((T^_{ko} S) \times_{t} (S^_{ko} R)) Cn (T^_{ko} R)))$

Metamath Proof Explorer

Theorem xkococn

Proof