llycmpkgen

Description: A locally compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	llycmpkgen	$⊢ J \in N-LocallyComp\toJ \in ran 𝑘Gen$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2		nllytop	$⊢ J \in N-LocallyComp\toJ \in Top$
3		simpl	$⊢ (J \in N-LocallyComp\landx \in ⋃ J\toJ \in N-LocallyComp)$
4	1	topopn	$⊢ J \in Top \to ⋃ J \in J$
5	2 4	syl	$⊢ J \in N-LocallyComp\to⋃ J \in J$
6	5	adantr	$⊢ (J \in N-LocallyComp\landx \in ⋃ J\to⋃ J \in J)$
7		simpr	$⊢ (J \in N-LocallyComp\landx \in ⋃ J\tox \in ⋃ J)$
8		nllyi	$⊢ (J \in N-LocallyComp\land⋃ J \in J\landx \in ⋃ J\to\exists k \in nei (J) (\{x\}) (k \subseteq ⋃ J \land J ↾_{𝑡} k \in Comp))$
9	3 6 7 8	syl3anc	$⊢ (J \in N-LocallyComp\landx \in ⋃ J\to\exists k \in nei (J) (\{x\}) (k \subseteq ⋃ J \land J ↾_{𝑡} k \in Comp))$
10		simpr	$⊢ (k \subseteq ⋃ J \land J ↾_{𝑡} k \in Comp) \to J ↾_{𝑡} k \in Comp$
11	10	reximi	$⊢ \exists k \in nei (J) (\{x\}) (k \subseteq ⋃ J \land J ↾_{𝑡} k \in Comp) \to \exists k \in nei (J) (\{x\}) J ↾_{𝑡} k \in Comp$
12	9 11	syl	$⊢ (J \in N-LocallyComp\landx \in ⋃ J\to\exists k \in nei (J) (\{x\}) J ↾_{𝑡} k \in Comp)$
13	1 2 12	llycmpkgen2	$⊢ J \in N-LocallyComp\toJ \in ran 𝑘Gen$

Metamath Proof Explorer