kgentopon

Description: The compact generator generates a topology. (Contributed by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Assertion	kgentopon	$⊢ J \in TopOn (X) \to 𝑘Gen (J) \in TopOn (X)$

Proof

Step	Hyp	Ref	Expression
1		uniss	$⊢ x \subseteq 𝑘Gen (J) \to ⋃ x \subseteq ⋃ 𝑘Gen (J)$
2		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))\}$
3		ssrab2	$⊢ \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\} \subseteq 𝒫 X$
4	2 3	eqsstrdi	$⊢ J \in TopOn (X) \to 𝑘Gen (J) \subseteq 𝒫 X$
5		sspwuni	$⊢ 𝑘Gen (J) \subseteq 𝒫 X \leftrightarrow ⋃ 𝑘Gen (J) \subseteq X$
6	4 5	sylib	$⊢ J \in TopOn (X) \to ⋃ 𝑘Gen (J) \subseteq X$
7	1 6	sylan9ssr	$⊢ (J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \to ⋃ x \subseteq X$
8		iunin2	$⊢ ⋃_{y \in x} (k \cap y) = k \cap ⋃_{y \in x} y$
9		uniiun	$⊢ ⋃ x = ⋃_{y \in x} y$
10	9	ineq2i	$⊢ k \cap ⋃ x = k \cap ⋃_{y \in x} y$
11		incom	$⊢ k \cap ⋃ x = ⋃ x \cap k$
12	8 10 11	3eqtr2i	$⊢ ⋃_{y \in x} (k \cap y) = ⋃ x \cap k$
13		cmptop	$⊢ J ↾_{𝑡} k \in Comp \to J ↾_{𝑡} k \in Top$
14	13	ad2antll	$⊢ ((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to J ↾_{𝑡} k \in Top$
15		incom	$⊢ y \cap k = k \cap y$
16		simplr	$⊢ ((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to x \subseteq 𝑘Gen (J)$
17	16	sselda	$⊢ (((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \land y \in x) \to y \in 𝑘Gen (J)$
18		simplrr	$⊢ (((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \land y \in x) \to J ↾_{𝑡} k \in Comp$
19		kgeni	$⊢ (y \in 𝑘Gen (J) \land J ↾_{𝑡} k \in Comp) \to y \cap k \in (J ↾_{𝑡} k)$
20	17 18 19	syl2anc	$⊢ (((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \land y \in x) \to y \cap k \in (J ↾_{𝑡} k)$
21	15 20	eqeltrrid	$⊢ (((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \land y \in x) \to k \cap y \in (J ↾_{𝑡} k)$
22	21	ralrimiva	$⊢ ((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to \forall y \in x k \cap y \in (J ↾_{𝑡} k)$
23		iunopn	$⊢ (J ↾_{𝑡} k \in Top \land \forall y \in x k \cap y \in (J ↾_{𝑡} k)) \to ⋃_{y \in x} (k \cap y) \in (J ↾_{𝑡} k)$
24	14 22 23	syl2anc	$⊢ ((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to ⋃_{y \in x} (k \cap y) \in (J ↾_{𝑡} k)$
25	12 24	eqeltrrid	$⊢ ((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to ⋃ x \cap k \in (J ↾_{𝑡} k)$
26	25	expr	$⊢ ((J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \land k \in 𝒫 X) \to (J ↾_{𝑡} k \in Comp \to ⋃ x \cap k \in (J ↾_{𝑡} k))$
27	26	ralrimiva	$⊢ (J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \to \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to ⋃ x \cap k \in (J ↾_{𝑡} k))$
28		elkgen	$⊢ J \in TopOn (X) \to (⋃ x \in 𝑘Gen (J) \leftrightarrow (⋃ x \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to ⋃ x \cap k \in (J ↾_{𝑡} k))))$
29	28	adantr	$⊢ (J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \to (⋃ x \in 𝑘Gen (J) \leftrightarrow (⋃ x \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to ⋃ x \cap k \in (J ↾_{𝑡} k))))$
30	7 27 29	mpbir2and	$⊢ (J \in TopOn (X) \land x \subseteq 𝑘Gen (J)) \to ⋃ x \in 𝑘Gen (J)$
31	30	ex	$⊢ J \in TopOn (X) \to (x \subseteq 𝑘Gen (J) \to ⋃ x \in 𝑘Gen (J))$
32	31	alrimiv	$⊢ J \in TopOn (X) \to \forall x (x \subseteq 𝑘Gen (J) \to ⋃ x \in 𝑘Gen (J))$
33		inss1	$⊢ x \cap y \subseteq x$
34		elssuni	$⊢ x \in 𝑘Gen (J) \to x \subseteq ⋃ 𝑘Gen (J)$
35	34	ad2antrl	$⊢ (J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \to x \subseteq ⋃ 𝑘Gen (J)$
36		ssidd	$⊢ J \in TopOn (X) \to X \subseteq X$
37		elpwi	$⊢ k \in 𝒫 X \to k \subseteq X$
38	37	ad2antrl	$⊢ (J \in TopOn (X) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to k \subseteq X$
39		sseqin2	$⊢ k \subseteq X \leftrightarrow X \cap k = k$
40	38 39	sylib	$⊢ (J \in TopOn (X) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to X \cap k = k$
41	37	adantr	$⊢ (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp) \to k \subseteq X$
42		resttopon	$⊢ (J \in TopOn (X) \land k \subseteq X) \to J ↾_{𝑡} k \in TopOn (k)$
43	41 42	sylan2	$⊢ (J \in TopOn (X) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to J ↾_{𝑡} k \in TopOn (k)$
44		toponmax	$⊢ J ↾_{𝑡} k \in TopOn (k) \to k \in (J ↾_{𝑡} k)$
45	43 44	syl	$⊢ (J \in TopOn (X) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to k \in (J ↾_{𝑡} k)$
46	40 45	eqeltrd	$⊢ (J \in TopOn (X) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to X \cap k \in (J ↾_{𝑡} k)$
47	46	expr	$⊢ (J \in TopOn (X) \land k \in 𝒫 X) \to (J ↾_{𝑡} k \in Comp \to X \cap k \in (J ↾_{𝑡} k))$
48	47	ralrimiva	$⊢ J \in TopOn (X) \to \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to X \cap k \in (J ↾_{𝑡} k))$
49		elkgen	$⊢ J \in TopOn (X) \to (X \in 𝑘Gen (J) \leftrightarrow (X \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to X \cap k \in (J ↾_{𝑡} k))))$
50	36 48 49	mpbir2and	$⊢ J \in TopOn (X) \to X \in 𝑘Gen (J)$
51		elssuni	$⊢ X \in 𝑘Gen (J) \to X \subseteq ⋃ 𝑘Gen (J)$
52	50 51	syl	$⊢ J \in TopOn (X) \to X \subseteq ⋃ 𝑘Gen (J)$
53	52 6	eqssd	$⊢ J \in TopOn (X) \to X = ⋃ 𝑘Gen (J)$
54	53	adantr	$⊢ (J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \to X = ⋃ 𝑘Gen (J)$
55	35 54	sseqtrrd	$⊢ (J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \to x \subseteq X$
56	33 55	sstrid	$⊢ (J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \to x \cap y \subseteq X$
57		inindir	$⊢ (x \cap y) \cap k = (x \cap k) \cap (y \cap k)$
58	13	ad2antll	$⊢ ((J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to J ↾_{𝑡} k \in Top$
59		simplrl	$⊢ ((J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to x \in 𝑘Gen (J)$
60		simprr	$⊢ ((J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to J ↾_{𝑡} k \in Comp$
61		kgeni	$⊢ (x \in 𝑘Gen (J) \land J ↾_{𝑡} k \in Comp) \to x \cap k \in (J ↾_{𝑡} k)$
62	59 60 61	syl2anc	$⊢ ((J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to x \cap k \in (J ↾_{𝑡} k)$
63		simplrr	$⊢ ((J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to y \in 𝑘Gen (J)$
64	63 60 19	syl2anc	$⊢ ((J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to y \cap k \in (J ↾_{𝑡} k)$
65		inopn	$⊢ (J ↾_{𝑡} k \in Top \land x \cap k \in (J ↾_{𝑡} k) \land y \cap k \in (J ↾_{𝑡} k)) \to (x \cap k) \cap (y \cap k) \in (J ↾_{𝑡} k)$
66	58 62 64 65	syl3anc	$⊢ ((J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to (x \cap k) \cap (y \cap k) \in (J ↾_{𝑡} k)$
67	57 66	eqeltrid	$⊢ ((J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \land (k \in 𝒫 X \land J ↾_{𝑡} k \in Comp)) \to (x \cap y) \cap k \in (J ↾_{𝑡} k)$
68	67	expr	$⊢ ((J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \land k \in 𝒫 X) \to (J ↾_{𝑡} k \in Comp \to (x \cap y) \cap k \in (J ↾_{𝑡} k))$
69	68	ralrimiva	$⊢ (J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \to \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to (x \cap y) \cap k \in (J ↾_{𝑡} k))$
70		elkgen	$⊢ J \in TopOn (X) \to (x \cap y \in 𝑘Gen (J) \leftrightarrow (x \cap y \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to (x \cap y) \cap k \in (J ↾_{𝑡} k))))$
71	70	adantr	$⊢ (J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \to (x \cap y \in 𝑘Gen (J) \leftrightarrow (x \cap y \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to (x \cap y) \cap k \in (J ↾_{𝑡} k))))$
72	56 69 71	mpbir2and	$⊢ (J \in TopOn (X) \land (x \in 𝑘Gen (J) \land y \in 𝑘Gen (J))) \to x \cap y \in 𝑘Gen (J)$
73	72	ralrimivva	$⊢ J \in TopOn (X) \to \forall x \in 𝑘Gen (J) \forall y \in 𝑘Gen (J) x \cap y \in 𝑘Gen (J)$
74		fvex	$⊢ 𝑘Gen (J) \in V$
75		istopg	$⊢ 𝑘Gen (J) \in V \to (𝑘Gen (J) \in Top \leftrightarrow (\forall x (x \subseteq 𝑘Gen (J) \to ⋃ x \in 𝑘Gen (J)) \land \forall x \in 𝑘Gen (J) \forall y \in 𝑘Gen (J) x \cap y \in 𝑘Gen (J)))$
76	74 75	ax-mp	$⊢ 𝑘Gen (J) \in Top \leftrightarrow (\forall x (x \subseteq 𝑘Gen (J) \to ⋃ x \in 𝑘Gen (J)) \land \forall x \in 𝑘Gen (J) \forall y \in 𝑘Gen (J) x \cap y \in 𝑘Gen (J))$
77	32 73 76	sylanbrc	$⊢ J \in TopOn (X) \to 𝑘Gen (J) \in Top$
78		istopon	$⊢ 𝑘Gen (J) \in TopOn (X) \leftrightarrow (𝑘Gen (J) \in Top \land X = ⋃ 𝑘Gen (J))$
79	77 53 78	sylanbrc	$⊢ J \in TopOn (X) \to 𝑘Gen (J) \in TopOn (X)$

Metamath Proof Explorer

Theorem kgentopon

Proof