xkoopn

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

	Ref	Expression
Hypotheses	xkoopn.x	$⊢ X = ⋃ R$
	xkoopn.r	$⊢ φ \to R \in Top$
	xkoopn.s	$⊢ φ \to S \in Top$
	xkoopn.a	$⊢ φ \to A \subseteq X$
	xkoopn.c	$⊢ φ \to R ↾_{𝑡} A \in Comp$
	xkoopn.u	$⊢ φ \to U \in S$
Assertion	xkoopn	$⊢ φ \to \{f \in (R Cn S) \| f [A] \subseteq U\} \in (S^_{ko} R)$

Proof

Step	Hyp	Ref	Expression
1		xkoopn.x	$⊢ X = ⋃ R$
2		xkoopn.r	$⊢ φ \to R \in Top$
3		xkoopn.s	$⊢ φ \to S \in Top$
4		xkoopn.a	$⊢ φ \to A \subseteq X$
5		xkoopn.c	$⊢ φ \to R ↾_{𝑡} A \in Comp$
6		xkoopn.u	$⊢ φ \to U \in S$
7		ovex	$⊢ R Cn S \in V$
8	7	pwex	$⊢ 𝒫 (R Cn S) \in V$
9		eqid	$⊢ \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} = \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}$
10		eqid	$⊢ (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) = (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})$
11	1 9 10	xkotf	$⊢ (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) : \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \times S ⟶ 𝒫 (R Cn S)$
12		frn	$⊢ (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) : \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \times S ⟶ 𝒫 (R Cn S) \to ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq 𝒫 (R Cn S)$
13	11 12	ax-mp	$⊢ ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq 𝒫 (R Cn S)$
14	8 13	ssexi	$⊢ ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \in V$
15		ssfii	$⊢ ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \in V \to ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))$
16	14 15	ax-mp	$⊢ ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))$
17		fvex	$⊢ fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})) \in V$
18		bastg	$⊢ fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})) \in V \to fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})) \subseteq topGen (fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
19	17 18	ax-mp	$⊢ fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})) \subseteq topGen (fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
20	16 19	sstri	$⊢ ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq topGen (fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
21		oveq2	$⊢ x = A \to R ↾_{𝑡} x = R ↾_{𝑡} A$
22	21	eleq1d	$⊢ x = A \to (R ↾_{𝑡} x \in Comp \leftrightarrow R ↾_{𝑡} A \in Comp)$
23	1	topopn	$⊢ R \in Top \to X \in R$
24		elpw2g	$⊢ X \in R \to (A \in 𝒫 X \leftrightarrow A \subseteq X)$
25	2 23 24	3syl	$⊢ φ \to (A \in 𝒫 X \leftrightarrow A \subseteq X)$
26	4 25	mpbird	$⊢ φ \to A \in 𝒫 X$
27	22 26 5	elrabd	$⊢ φ \to A \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}$
28		eqidd	$⊢ φ \to \{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [A] \subseteq U\}$
29		imaeq2	$⊢ k = A \to f [k] = f [A]$
30	29	sseq1d	$⊢ k = A \to (f [k] \subseteq v \leftrightarrow f [A] \subseteq v)$
31	30	rabbidv	$⊢ k = A \to \{f \in (R Cn S) \| f [k] \subseteq v\} = \{f \in (R Cn S) \| f [A] \subseteq v\}$
32	31	eqeq2d	$⊢ k = A \to (\{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [k] \subseteq v\} \leftrightarrow \{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [A] \subseteq v\})$
33		sseq2	$⊢ v = U \to (f [A] \subseteq v \leftrightarrow f [A] \subseteq U)$
34	33	rabbidv	$⊢ v = U \to \{f \in (R Cn S) \| f [A] \subseteq v\} = \{f \in (R Cn S) \| f [A] \subseteq U\}$
35	34	eqeq2d	$⊢ v = U \to (\{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [A] \subseteq v\} \leftrightarrow \{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [A] \subseteq U\})$
36	32 35	rspc2ev	$⊢ (A \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \land U \in S \land \{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [A] \subseteq U\}) \to \exists k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \exists v \in S \{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [k] \subseteq v\}$
37	27 6 28 36	syl3anc	$⊢ φ \to \exists k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \exists v \in S \{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [k] \subseteq v\}$
38	7	rabex	$⊢ \{f \in (R Cn S) \| f [A] \subseteq U\} \in V$
39		eqeq1	$⊢ y = \{f \in (R Cn S) \| f [A] \subseteq U\} \to (y = \{f \in (R Cn S) \| f [k] \subseteq v\} \leftrightarrow \{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [k] \subseteq v\})$
40	39	2rexbidv	$⊢ y = \{f \in (R Cn S) \| f [A] \subseteq U\} \to (\exists k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \exists v \in S y = \{f \in (R Cn S) \| f [k] \subseteq v\} \leftrightarrow \exists k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \exists v \in S \{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [k] \subseteq v\})$
41	10	rnmpo	$⊢ ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) = \{y \| \exists k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \exists v \in S y = \{f \in (R Cn S) \| f [k] \subseteq v\}\}$
42	38 40 41	elab2	$⊢ \{f \in (R Cn S) \| f [A] \subseteq U\} \in ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \leftrightarrow \exists k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \exists v \in S \{f \in (R Cn S) \| f [A] \subseteq U\} = \{f \in (R Cn S) \| f [k] \subseteq v\}$
43	37 42	sylibr	$⊢ φ \to \{f \in (R Cn S) \| f [A] \subseteq U\} \in ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})$
44	20 43	sseldi	$⊢ φ \to \{f \in (R Cn S) \| f [A] \subseteq U\} \in topGen (fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
45	1 9 10	xkoval	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R = topGen (fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
46	2 3 45	syl2anc	$⊢ φ \to S^_{ko} R = topGen (fi (ran (k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
47	44 46	eleqtrrd	$⊢ φ \to \{f \in (R Cn S) \| f [A] \subseteq U\} \in (S^_{ko} R)$

Metamath Proof Explorer

Theorem xkoopn

Proof