xkoval

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

	Ref	Expression
Hypotheses	xkoval.x	$⊢ X = ⋃ R$
	xkoval.k	$⊢ K = \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}$
	xkoval.t	$⊢ T = (k \in K, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})$
Assertion	xkoval	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R = topGen (fi (ran T))$

Proof

Step	Hyp	Ref	Expression
1		xkoval.x	$⊢ X = ⋃ R$
2		xkoval.k	$⊢ K = \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}$
3		xkoval.t	$⊢ T = (k \in K, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})$
4		simpr	$⊢ (s = S \land r = R) \to r = R$
5	4	unieqd	$⊢ (s = S \land r = R) \to ⋃ r = ⋃ R$
6	5 1	eqtr4di	$⊢ (s = S \land r = R) \to ⋃ r = X$
7	6	pweqd	$⊢ (s = S \land r = R) \to 𝒫 ⋃ r = 𝒫 X$
8	4	oveq1d	$⊢ (s = S \land r = R) \to r ↾_{𝑡} x = R ↾_{𝑡} x$
9	8	eleq1d	$⊢ (s = S \land r = R) \to (r ↾_{𝑡} x \in Comp \leftrightarrow R ↾_{𝑡} x \in Comp)$
10	7 9	rabeqbidv	$⊢ (s = S \land r = R) \to \{x \in 𝒫 ⋃ r \| r ↾_{𝑡} x \in Comp\} = \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\}$
11	10 2	eqtr4di	$⊢ (s = S \land r = R) \to \{x \in 𝒫 ⋃ r \| r ↾_{𝑡} x \in Comp\} = K$
12		simpl	$⊢ (s = S \land r = R) \to s = S$
13	4 12	oveq12d	$⊢ (s = S \land r = R) \to r Cn s = R Cn S$
14	13	rabeqdv	$⊢ (s = S \land r = R) \to \{f \in (r Cn s) \| f [k] \subseteq v\} = \{f \in (R Cn S) \| f [k] \subseteq v\}$
15	11 12 14	mpoeq123dv	$⊢ (s = S \land r = R) \to (k \in \{x \in 𝒫 ⋃ r \| r ↾_{𝑡} x \in Comp\}, v \in s ⟼ \{f \in (r Cn s) \| f [k] \subseteq v\}) = (k \in K, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})$
16	15 3	eqtr4di	$⊢ (s = S \land r = R) \to (k \in \{x \in 𝒫 ⋃ r \| r ↾_{𝑡} x \in Comp\}, v \in s ⟼ \{f \in (r Cn s) \| f [k] \subseteq v\}) = T$
17	16	rneqd	$⊢ (s = S \land r = R) \to ran (k \in \{x \in 𝒫 ⋃ r \| r ↾_{𝑡} x \in Comp\}, v \in s ⟼ \{f \in (r Cn s) \| f [k] \subseteq v\}) = ran T$
18	17	fveq2d	$⊢ (s = S \land r = R) \to 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 T)$
19	18	fveq2d	$⊢ (s = S \land r = R) \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\}))) = topGen (fi (ran T))$
20		df-xko	$⊢^_{ko} = (s \in Top, r \in Top ⟼ topGen (fi (ran (k \in \{x \in 𝒫 ⋃ r \| r ↾_{𝑡} x \in Comp\}, v \in s ⟼ \{f \in (r Cn s) \| f [k] \subseteq v\}))))$
21		fvex	$⊢ topGen (fi (ran T)) \in V$
22	19 20 21	ovmpoa	$⊢ (S \in Top \land R \in Top) \to S^_{ko} R = topGen (fi (ran T))$
23	22	ancoms	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R = topGen (fi (ran T))$

Metamath Proof Explorer

Theorem xkoval

Proof