kgencmp2

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

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

Proof

Step	Hyp	Ref	Expression
1		kgencmp	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K = 𝑘Gen (J) ↾_{𝑡} K$
2		simpr	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \in Comp$
3	1 2	eqeltrrd	$⊢ (J \in Top \land J ↾_{𝑡} K \in Comp) \to 𝑘Gen (J) ↾_{𝑡} K \in Comp$
4		cmptop	$⊢ 𝑘Gen (J) ↾_{𝑡} K \in Comp \to 𝑘Gen (J) ↾_{𝑡} K \in Top$
5		restrcl	$⊢ 𝑘Gen (J) ↾_{𝑡} K \in Top \to (𝑘Gen (J) \in V \land K \in V)$
6	5	simprd	$⊢ 𝑘Gen (J) ↾_{𝑡} K \in Top \to K \in V$
7	4 6	syl	$⊢ 𝑘Gen (J) ↾_{𝑡} K \in Comp \to K \in V$
8		resttop	$⊢ (J \in Top \land K \in V) \to J ↾_{𝑡} K \in Top$
9	7 8	sylan2	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \in Top$
10		toptopon2	$⊢ J ↾_{𝑡} K \in Top \leftrightarrow J ↾_{𝑡} K \in TopOn (⋃ (J ↾_{𝑡} K))$
11	9 10	sylib	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \in TopOn (⋃ (J ↾_{𝑡} K))$
12		eqid	$⊢ ⋃ J = ⋃ J$
13	12	kgenuni	$⊢ J \in Top \to ⋃ J = ⋃ 𝑘Gen (J)$
14	13	adantr	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to ⋃ J = ⋃ 𝑘Gen (J)$
15	14	ineq2d	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to K \cap ⋃ J = K \cap ⋃ 𝑘Gen (J)$
16	12	restuni2	$⊢ (J \in Top \land K \in V) \to K \cap ⋃ J = ⋃ (J ↾_{𝑡} K)$
17	7 16	sylan2	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to K \cap ⋃ J = ⋃ (J ↾_{𝑡} K)$
18		kgenftop	$⊢ J \in Top \to 𝑘Gen (J) \in Top$
19		eqid	$⊢ ⋃ 𝑘Gen (J) = ⋃ 𝑘Gen (J)$
20	19	restuni2	$⊢ (𝑘Gen (J) \in Top \land K \in V) \to K \cap ⋃ 𝑘Gen (J) = ⋃ (𝑘Gen (J) ↾_{𝑡} K)$
21	18 7 20	syl2an	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to K \cap ⋃ 𝑘Gen (J) = ⋃ (𝑘Gen (J) ↾_{𝑡} K)$
22	15 17 21	3eqtr3d	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to ⋃ (J ↾_{𝑡} K) = ⋃ (𝑘Gen (J) ↾_{𝑡} K)$
23	22	fveq2d	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to TopOn (⋃ (J ↾_{𝑡} K)) = TopOn (⋃ (𝑘Gen (J) ↾_{𝑡} K))$
24	11 23	eleqtrd	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \in TopOn (⋃ (𝑘Gen (J) ↾_{𝑡} K))$
25		simpr	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to 𝑘Gen (J) ↾_{𝑡} K \in Comp$
26		kgenss	$⊢ J \in Top \to J \subseteq 𝑘Gen (J)$
27	26	adantr	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to J \subseteq 𝑘Gen (J)$
28		ssrest	$⊢ (𝑘Gen (J) \in Top \land J \subseteq 𝑘Gen (J)) \to J ↾_{𝑡} K \subseteq 𝑘Gen (J) ↾_{𝑡} K$
29	18 27 28	syl2an2r	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \subseteq 𝑘Gen (J) ↾_{𝑡} K$
30		eqid	$⊢ ⋃ (𝑘Gen (J) ↾_{𝑡} K) = ⋃ (𝑘Gen (J) ↾_{𝑡} K)$
31	30	sscmp	$⊢ (J ↾_{𝑡} K \in TopOn (⋃ (𝑘Gen (J) ↾_{𝑡} K)) \land 𝑘Gen (J) ↾_{𝑡} K \in Comp \land J ↾_{𝑡} K \subseteq 𝑘Gen (J) ↾_{𝑡} K) \to J ↾_{𝑡} K \in Comp$
32	24 25 29 31	syl3anc	$⊢ (J \in Top \land 𝑘Gen (J) ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \in Comp$
33	3 32	impbida	$⊢ J \in Top \to (J ↾_{𝑡} K \in Comp \leftrightarrow 𝑘Gen (J) ↾_{𝑡} K \in Comp)$

Metamath Proof Explorer

Theorem kgencmp2

Proof