xkouni

Description: The base set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Hypothesis	xkouni.1	$⊢ J = S^_{ko} R$
	Assertion	xkouni	$⊢ (R \in Top \land S \in Top) \to R Cn S = ⋃ J$

Proof

Step	Hyp	Ref	Expression
1		xkouni.1	$⊢ J = S^_{ko} R$
2		ima0	$⊢ f [\emptyset] = \emptyset$
3		0ss	$⊢ \emptyset \subseteq ⋃ S$
4	2 3	eqsstri	$⊢ f [\emptyset] \subseteq ⋃ S$
5	4	a1i	$⊢ ((R \in Top \land S \in Top) \land f \in (R Cn S)) \to f [\emptyset] \subseteq ⋃ S$
6	5	ralrimiva	$⊢ (R \in Top \land S \in Top) \to \forall f \in (R Cn S) f [\emptyset] \subseteq ⋃ S$
7		rabid2	$⊢ R Cn S = \{f \in (R Cn S) \| f [\emptyset] \subseteq ⋃ S\} \leftrightarrow \forall f \in (R Cn S) f [\emptyset] \subseteq ⋃ S$
8	6 7	sylibr	$⊢ (R \in Top \land S \in Top) \to R Cn S = \{f \in (R Cn S) \| f [\emptyset] \subseteq ⋃ S\}$
9		eqid	$⊢ ⋃ R = ⋃ R$
10		simpl	$⊢ (R \in Top \land S \in Top) \to R \in Top$
11		simpr	$⊢ (R \in Top \land S \in Top) \to S \in Top$
12		0ss	$⊢ \emptyset \subseteq ⋃ R$
13	12	a1i	$⊢ (R \in Top \land S \in Top) \to \emptyset \subseteq ⋃ R$
14		rest0	$⊢ R \in Top \to R ↾_{𝑡} \emptyset = \{\emptyset\}$
15	14	adantr	$⊢ (R \in Top \land S \in Top) \to R ↾_{𝑡} \emptyset = \{\emptyset\}$
16		0cmp	$⊢ \{\emptyset\} \in Comp$
17	15 16	eqeltrdi	$⊢ (R \in Top \land S \in Top) \to R ↾_{𝑡} \emptyset \in Comp$
18		eqid	$⊢ ⋃ S = ⋃ S$
19	18	topopn	$⊢ S \in Top \to ⋃ S \in S$
20	19	adantl	$⊢ (R \in Top \land S \in Top) \to ⋃ S \in S$
21	9 10 11 13 17 20	xkoopn	$⊢ (R \in Top \land S \in Top) \to \{f \in (R Cn S) \| f [\emptyset] \subseteq ⋃ S\} \in (S^_{ko} R)$
22	8 21	eqeltrd	$⊢ (R \in Top \land S \in Top) \to R Cn S \in (S^_{ko} R)$
23	22 1	eleqtrrdi	$⊢ (R \in Top \land S \in Top) \to R Cn S \in J$
24		elssuni	$⊢ R Cn S \in J \to R Cn S \subseteq ⋃ J$
25	23 24	syl	$⊢ (R \in Top \land S \in Top) \to R Cn S \subseteq ⋃ J$
26		eqid	$⊢ \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\} = \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}$
27		eqid	$⊢ (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) = (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})$
28	9 26 27	xkoval	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R = topGen (fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
29	28	unieqd	$⊢ (R \in Top \land S \in Top) \to ⋃ (S^_{ko} R) = ⋃ topGen (fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
30	1	unieqi	$⊢ ⋃ J = ⋃ (S^_{ko} R)$
31		ovex	$⊢ R Cn S \in V$
32	31	pwex	$⊢ 𝒫 (R Cn S) \in V$
33	9 26 27	xkotf	$⊢ (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) : \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\} \times S ⟶ 𝒫 (R Cn S)$
34		frn	$⊢ (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) : \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\} \times S ⟶ 𝒫 (R Cn S) \to ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq 𝒫 (R Cn S)$
35	33 34	ax-mp	$⊢ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq 𝒫 (R Cn S)$
36	32 35	ssexi	$⊢ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \in V$
37		fiuni	$⊢ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \in V \to ⋃ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) = ⋃ fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))$
38	36 37	ax-mp	$⊢ ⋃ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) = ⋃ fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))$
39		fvex	$⊢ fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})) \in V$
40		unitg	$⊢ fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})) \in V \to ⋃ topGen (fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))) = ⋃ fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))$
41	39 40	ax-mp	$⊢ ⋃ topGen (fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))) = ⋃ fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))$
42	38 41	eqtr4i	$⊢ ⋃ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) = ⋃ topGen (fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
43	29 30 42	3eqtr4g	$⊢ (R \in Top \land S \in Top) \to ⋃ J = ⋃ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})$
44	35	a1i	$⊢ (R \in Top \land S \in Top) \to ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq 𝒫 (R Cn S)$
45		sspwuni	$⊢ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq 𝒫 (R Cn S) \leftrightarrow ⋃ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq R Cn S$
46	44 45	sylib	$⊢ (R \in Top \land S \in Top) \to ⋃ ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq R Cn S$
47	43 46	eqsstrd	$⊢ (R \in Top \land S \in Top) \to ⋃ J \subseteq R Cn S$
48	25 47	eqssd	$⊢ (R \in Top \land S \in Top) \to R Cn S = ⋃ J$

Metamath Proof Explorer

Theorem xkouni

Proof