kgenss

Description: The compact generator generates a finer topology than the original. (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Assertion	kgenss	$⊢ J \in Top \to J \subseteq 𝑘Gen (J)$

Step	Hyp	Ref	Expression
1		elssuni	$⊢ x \in J \to x \subseteq ⋃ J$
2	1	a1i	$⊢ J \in Top \to (x \in J \to x \subseteq ⋃ J)$
3		elrestr	$⊢ (J \in Top \land k \in 𝒫 ⋃ J \land x \in J) \to x \cap k \in (J ↾_{𝑡} k)$
4	3	3expa	$⊢ ((J \in Top \land k \in 𝒫 ⋃ J) \land x \in J) \to x \cap k \in (J ↾_{𝑡} k)$
5	4	an32s	$⊢ ((J \in Top \land x \in J) \land k \in 𝒫 ⋃ J) \to x \cap k \in (J ↾_{𝑡} k)$
6	5	a1d	$⊢ ((J \in Top \land x \in J) \land k \in 𝒫 ⋃ J) \to (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))$
7	6	ralrimiva	$⊢ (J \in Top \land x \in J) \to \forall k \in 𝒫 ⋃ J (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))$
8	7	ex	$⊢ J \in Top \to (x \in J \to \forall k \in 𝒫 ⋃ J (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)))$
9	2 8	jcad	$⊢ J \in Top \to (x \in J \to (x \subseteq ⋃ J \land \forall k \in 𝒫 ⋃ J (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))))$
10		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
11		elkgen	$⊢ J \in TopOn (⋃ J) \to (x \in 𝑘Gen (J) \leftrightarrow (x \subseteq ⋃ J \land \forall k \in 𝒫 ⋃ J (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))))$
12	10 11	sylbi	$⊢ J \in Top \to (x \in 𝑘Gen (J) \leftrightarrow (x \subseteq ⋃ J \land \forall k \in 𝒫 ⋃ J (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))))$
13	9 12	sylibrd	$⊢ J \in Top \to (x \in J \to x \in 𝑘Gen (J))$
14	13	ssrdv	$⊢ J \in Top \to J \subseteq 𝑘Gen (J)$

Metamath Proof Explorer