kgencmp

Description: The compact generator topology is the same as the original topology on compact subspaces. (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Assertion	kgencmp	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K = 𝑘Gen (J) ↾_{𝑡} K$

Proof

Step	Hyp	Ref	Expression
1		kgenftop	$⊢ J \in Top \to 𝑘Gen (J) \in Top$
2	1	adantr	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to 𝑘Gen (J) \in Top$
3		kgenss	$⊢ J \in Top \to J \subseteq 𝑘Gen (J)$
4	3	adantr	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to J \subseteq 𝑘Gen (J)$
5		ssrest	$⊢ (𝑘Gen (J) \in Top \land J \subseteq 𝑘Gen (J)) \to J ↾_{𝑡} K \subseteq 𝑘Gen (J) ↾_{𝑡} K$
6	2 4 5	syl2anc	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \subseteq 𝑘Gen (J) ↾_{𝑡} K$
7		cmptop	$⊢ J ↾_{𝑡} K \in Comp \to J ↾_{𝑡} K \in Top$
8	7	adantl	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \in Top$
9		restrcl	$⊢ J ↾_{𝑡} K \in Top \to (J \in V \land K \in V)$
10	9	simprd	$⊢ J ↾_{𝑡} K \in Top \to K \in V$
11	8 10	syl	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to K \in V$
12		restval	$⊢ (𝑘Gen (J) \in Top \land K \in V) \to 𝑘Gen (J) ↾_{𝑡} K = ran (x \in 𝑘Gen (J) ⟼ x \cap K)$
13	2 11 12	syl2anc	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to 𝑘Gen (J) ↾_{𝑡} K = ran (x \in 𝑘Gen (J) ⟼ x \cap K)$
14		simpr	$⊢ ((J \in Top \land J ↾_{𝑡} K \in Comp) \land x \in 𝑘Gen (J)) \to x \in 𝑘Gen (J)$
15		simplr	$⊢ ((J \in Top \land J ↾_{𝑡} K \in Comp) \land x \in 𝑘Gen (J)) \to J ↾_{𝑡} K \in Comp$
16		kgeni	$⊢ (x \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to x \cap K \in (J ↾_{𝑡} K)$
17	14 15 16	syl2anc	$⊢ ((J \in Top \land J ↾_{𝑡} K \in Comp) \land x \in 𝑘Gen (J)) \to x \cap K \in (J ↾_{𝑡} K)$
18	17	fmpttd	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to (x \in 𝑘Gen (J) ⟼ x \cap K) : 𝑘Gen (J) ⟶ J ↾_{𝑡} K$
19	18	frnd	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to ran (x \in 𝑘Gen (J) ⟼ x \cap K) \subseteq J ↾_{𝑡} K$
20	13 19	eqsstrd	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to 𝑘Gen (J) ↾_{𝑡} K \subseteq J ↾_{𝑡} K$
21	6 20	eqssd	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K = 𝑘Gen (J) ↾_{𝑡} K$

Metamath Proof Explorer

Theorem kgencmp

Proof