Metamath Proof Explorer

Theorem kgenval

Description: Value of the compact generator. (The "k" in kGen comes from the name "k-space" for these spaces, after the German word kompakt.) (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Assertion	kgenval	$⊢ J \in TopOn (X) \to 𝑘Gen (J) = \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\}$

Proof

Step	Hyp	Ref	Expression
1		df-kgen	$⊢ 𝑘Gen = (j \in Top ⟼ \{x \in 𝒫 ⋃ j \| \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))\})$
2		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
3		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
4	3	eqcomd	$⊢ J \in TopOn (X) \to ⋃ J = X$
5	2 4	sylan9eqr	$⊢ (J \in TopOn (X) \land j = J) \to ⋃ j = X$
6	5	pweqd	$⊢ (J \in TopOn (X) \land j = J) \to 𝒫 ⋃ j = 𝒫 X$
7		oveq1	$⊢ j = J \to j ↾_{𝑡} k = J ↾_{𝑡} k$
8	7	eleq1d	$⊢ j = J \to (j ↾_{𝑡} k \in Comp \leftrightarrow J ↾_{𝑡} k \in Comp)$
9	7	eleq2d	$⊢ j = J \to (x \cap k \in (j ↾_{𝑡} k) \leftrightarrow x \cap k \in (J ↾_{𝑡} k))$
10	8 9	imbi12d	$⊢ j = J \to ((j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k)) \leftrightarrow (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)))$
11	10	adantl	$⊢ (J \in TopOn (X) \land j = J) \to ((j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k)) \leftrightarrow (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)))$
12	6 11	raleqbidv	$⊢ (J \in TopOn (X) \land j = J) \to (\forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k)) \leftrightarrow \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)))$
13	6 12	rabeqbidv	$⊢ (J \in TopOn (X) \land j = J) \to \{x \in 𝒫 ⋃ j \| \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))\} = \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\}$
14		topontop	$⊢ J \in TopOn (X) \to J \in Top$
15		toponmax	$⊢ J \in TopOn (X) \to X \in J$
16		pwexg	$⊢ X \in J \to 𝒫 X \in V$
17		rabexg	$⊢ 𝒫 X \in V \to \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\} \in V$
18	15 16 17	3syl	$⊢ J \in TopOn (X) \to \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\} \in V$
19	1 13 14 18	fvmptd2	$⊢ J \in TopOn (X) \to 𝑘Gen (J) = \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\}$