Metamath Proof Explorer

Theorem xkobval

Description: Alternative expression for the subbase of the compact-open topology. (Contributed by Mario Carneiro, 23-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	xkobval	$⊢ ran T = \{s \| \exists k \in 𝒫 X \exists v \in S (R ↾_{𝑡} k \in Comp \land s = \{f \in (R Cn S) \| f [k] \subseteq v\})\}$

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	3	rnmpo	$⊢ ran T = \{s \| \exists k \in K \exists v \in S s = \{f \in (R Cn S) \| f [k] \subseteq v\}\}$
5		oveq2	$⊢ x = k \to R ↾_{𝑡} x = R ↾_{𝑡} k$
6	5	eleq1d	$⊢ x = k \to (R ↾_{𝑡} x \in Comp \leftrightarrow R ↾_{𝑡} k \in Comp)$
7	6	rexrab	$⊢ \exists k \in \{x \in 𝒫 X \| R ↾_{𝑡} x \in Comp\} \exists v \in S s = \{f \in (R Cn S) \| f [k] \subseteq v\} \leftrightarrow \exists k \in 𝒫 X (R ↾_{𝑡} k \in Comp \land \exists v \in S s = \{f \in (R Cn S) \| f [k] \subseteq v\})$
8	2	rexeqi	$⊢ \exists k \in K \exists v \in S 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 s = \{f \in (R Cn S) \| f [k] \subseteq v\}$
9		r19.42v	$⊢ \exists v \in S (R ↾_{𝑡} k \in Comp \land s = \{f \in (R Cn S) \| f [k] \subseteq v\}) \leftrightarrow (R ↾_{𝑡} k \in Comp \land \exists v \in S s = \{f \in (R Cn S) \| f [k] \subseteq v\})$
10	9	rexbii	$⊢ \exists k \in 𝒫 X \exists v \in S (R ↾_{𝑡} k \in Comp \land s = \{f \in (R Cn S) \| f [k] \subseteq v\}) \leftrightarrow \exists k \in 𝒫 X (R ↾_{𝑡} k \in Comp \land \exists v \in S s = \{f \in (R Cn S) \| f [k] \subseteq v\})$
11	7 8 10	3bitr4i	$⊢ \exists k \in K \exists v \in S s = \{f \in (R Cn S) \| f [k] \subseteq v\} \leftrightarrow \exists k \in 𝒫 X \exists v \in S (R ↾_{𝑡} k \in Comp \land s = \{f \in (R Cn S) \| f [k] \subseteq v\})$
12	11	abbii	$⊢ \{s \| \exists k \in K \exists v \in S s = \{f \in (R Cn S) \| f [k] \subseteq v\}\} = \{s \| \exists k \in 𝒫 X \exists v \in S (R ↾_{𝑡} k \in Comp \land s = \{f \in (R Cn S) \| f [k] \subseteq v\})\}$
13	4 12	eqtri	$⊢ ran T = \{s \| \exists k \in 𝒫 X \exists v \in S (R ↾_{𝑡} k \in Comp \land s = \{f \in (R Cn S) \| f [k] \subseteq v\})\}$