llycmpkgen2

Description: A locally compact space is compactly generated. (This variant of llycmpkgen uses the weaker definition of locally compact, "every point has a compact neighborhood", instead of "every point has a local base of compact neighborhoods".) (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Hypotheses	iskgen3.1	$⊢ X = ⋃ J$
	llycmpkgen2.2	$⊢ φ \to J \in Top$
	llycmpkgen2.3	$⊢ (φ \land x \in X) \to \exists k \in nei (J) (\{x\}) J ↾_{𝑡} k \in Comp$
Assertion	llycmpkgen2	$⊢ φ \to J \in ran 𝑘Gen$

Proof

Step	Hyp	Ref	Expression
1		iskgen3.1	$⊢ X = ⋃ J$
2		llycmpkgen2.2	$⊢ φ \to J \in Top$
3		llycmpkgen2.3	$⊢ (φ \land x \in X) \to \exists k \in nei (J) (\{x\}) J ↾_{𝑡} k \in Comp$
4		elssuni	$⊢ u \in 𝑘Gen (J) \to u \subseteq ⋃ 𝑘Gen (J)$
5	4	adantl	$⊢ (φ \land u \in 𝑘Gen (J)) \to u \subseteq ⋃ 𝑘Gen (J)$
6	1	kgenuni	$⊢ J \in Top \to X = ⋃ 𝑘Gen (J)$
7	2 6	syl	$⊢ φ \to X = ⋃ 𝑘Gen (J)$
8	7	adantr	$⊢ (φ \land u \in 𝑘Gen (J)) \to X = ⋃ 𝑘Gen (J)$
9	5 8	sseqtrrd	$⊢ (φ \land u \in 𝑘Gen (J)) \to u \subseteq X$
10	9	sselda	$⊢ ((φ \land u \in 𝑘Gen (J)) \land x \in u) \to x \in X$
11	3	adantlr	$⊢ ((φ \land u \in 𝑘Gen (J)) \land x \in X) \to \exists k \in nei (J) (\{x\}) J ↾_{𝑡} k \in Comp$
12	10 11	syldan	$⊢ ((φ \land u \in 𝑘Gen (J)) \land x \in u) \to \exists k \in nei (J) (\{x\}) J ↾_{𝑡} k \in Comp$
13	2	ad3antrrr	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to J \in Top$
14		difss	$⊢ X ∖ (k ∖ u) \subseteq X$
15	1	ntropn	$⊢ (J \in Top \land X ∖ (k ∖ u) \subseteq X) \to int (J) (X ∖ (k ∖ u)) \in J$
16	13 14 15	sylancl	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (X ∖ (k ∖ u)) \in J$
17		simprl	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to k \in nei (J) (\{x\})$
18	1	neii1	$⊢ (J \in Top \land k \in nei (J) (\{x\})) \to k \subseteq X$
19	13 17 18	syl2anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to k \subseteq X$
20	1	ntropn	$⊢ (J \in Top \land k \subseteq X) \to int (J) (k) \in J$
21	13 19 20	syl2anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (k) \in J$
22		inopn	$⊢ (J \in Top \land int (J) (X ∖ (k ∖ u)) \in J \land int (J) (k) \in J) \to int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \in J$
23	13 16 21 22	syl3anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \in J$
24		simplr	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to x \in u$
25	1	ntrss2	$⊢ (J \in Top \land k \subseteq X) \to int (J) (k) \subseteq k$
26	13 19 25	syl2anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (k) \subseteq k$
27	10	adantr	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to x \in X$
28	27	snssd	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to \{x\} \subseteq X$
29	1	neiint	$⊢ (J \in Top \land \{x\} \subseteq X \land k \subseteq X) \to (k \in nei (J) (\{x\}) \leftrightarrow \{x\} \subseteq int (J) (k))$
30	13 28 19 29	syl3anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to (k \in nei (J) (\{x\}) \leftrightarrow \{x\} \subseteq int (J) (k))$
31	17 30	mpbid	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to \{x\} \subseteq int (J) (k)$
32		vex	$⊢ x \in V$
33	32	snss	$⊢ x \in int (J) (k) \leftrightarrow \{x\} \subseteq int (J) (k)$
34	31 33	sylibr	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to x \in int (J) (k)$
35	26 34	sseldd	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to x \in k$
36	24 35	elind	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to x \in (u \cap k)$
37		simpllr	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to u \in 𝑘Gen (J)$
38		simprr	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to J ↾_{𝑡} k \in Comp$
39		kgeni	$⊢ (u \in 𝑘Gen (J) \land J ↾_{𝑡} k \in Comp) \to u \cap k \in (J ↾_{𝑡} k)$
40	37 38 39	syl2anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to u \cap k \in (J ↾_{𝑡} k)$
41		vex	$⊢ k \in V$
42		resttop	$⊢ (J \in Top \land k \in V) \to J ↾_{𝑡} k \in Top$
43	13 41 42	sylancl	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to J ↾_{𝑡} k \in Top$
44		inss2	$⊢ u \cap k \subseteq k$
45	1	restuni	$⊢ (J \in Top \land k \subseteq X) \to k = ⋃ (J ↾_{𝑡} k)$
46	13 19 45	syl2anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to k = ⋃ (J ↾_{𝑡} k)$
47	44 46	sseqtrid	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to u \cap k \subseteq ⋃ (J ↾_{𝑡} k)$
48		eqid	$⊢ ⋃ (J ↾_{𝑡} k) = ⋃ (J ↾_{𝑡} k)$
49	48	isopn3	$⊢ (J ↾_{𝑡} k \in Top \land u \cap k \subseteq ⋃ (J ↾_{𝑡} k)) \to (u \cap k \in (J ↾_{𝑡} k) \leftrightarrow int (J ↾_{𝑡} k) (u \cap k) = u \cap k)$
50	43 47 49	syl2anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to (u \cap k \in (J ↾_{𝑡} k) \leftrightarrow int (J ↾_{𝑡} k) (u \cap k) = u \cap k)$
51	40 50	mpbid	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J ↾_{𝑡} k) (u \cap k) = u \cap k$
52	44	a1i	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to u \cap k \subseteq k$
53		eqid	$⊢ J ↾_{𝑡} k = J ↾_{𝑡} k$
54	1 53	restntr	$⊢ (J \in Top \land k \subseteq X \land u \cap k \subseteq k) \to int (J ↾_{𝑡} k) (u \cap k) = int (J) ((u \cap k) \cup (X ∖ k)) \cap k$
55	13 19 52 54	syl3anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J ↾_{𝑡} k) (u \cap k) = int (J) ((u \cap k) \cup (X ∖ k)) \cap k$
56	51 55	eqtr3d	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to u \cap k = int (J) ((u \cap k) \cup (X ∖ k)) \cap k$
57	36 56	eleqtrd	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to x \in (int (J) ((u \cap k) \cup (X ∖ k)) \cap k)$
58	57	elin1d	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to x \in int (J) ((u \cap k) \cup (X ∖ k))$
59		undif3	$⊢ (u \cap k) \cup (X ∖ k) = ((u \cap k) \cup X) ∖ (k ∖ (u \cap k))$
60		incom	$⊢ u \cap k = k \cap u$
61	60	difeq2i	$⊢ k ∖ (u \cap k) = k ∖ (k \cap u)$
62		difin	$⊢ k ∖ (k \cap u) = k ∖ u$
63	61 62	eqtri	$⊢ k ∖ (u \cap k) = k ∖ u$
64	63	difeq2i	$⊢ ((u \cap k) \cup X) ∖ (k ∖ (u \cap k)) = ((u \cap k) \cup X) ∖ (k ∖ u)$
65	59 64	eqtri	$⊢ (u \cap k) \cup (X ∖ k) = ((u \cap k) \cup X) ∖ (k ∖ u)$
66	44 19	sstrid	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to u \cap k \subseteq X$
67		ssequn1	$⊢ u \cap k \subseteq X \leftrightarrow (u \cap k) \cup X = X$
68	66 67	sylib	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to (u \cap k) \cup X = X$
69	68	difeq1d	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to ((u \cap k) \cup X) ∖ (k ∖ u) = X ∖ (k ∖ u)$
70	65 69	syl5eq	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to (u \cap k) \cup (X ∖ k) = X ∖ (k ∖ u)$
71	70	fveq2d	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) ((u \cap k) \cup (X ∖ k)) = int (J) (X ∖ (k ∖ u))$
72	58 71	eleqtrd	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to x \in int (J) (X ∖ (k ∖ u))$
73	72 34	elind	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to x \in (int (J) (X ∖ (k ∖ u)) \cap int (J) (k))$
74		sslin	$⊢ int (J) (k) \subseteq k \to int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \subseteq int (J) (X ∖ (k ∖ u)) \cap k$
75	26 74	syl	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \subseteq int (J) (X ∖ (k ∖ u)) \cap k$
76	1	ntrss2	$⊢ (J \in Top \land X ∖ (k ∖ u) \subseteq X) \to int (J) (X ∖ (k ∖ u)) \subseteq X ∖ (k ∖ u)$
77	13 14 76	sylancl	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (X ∖ (k ∖ u)) \subseteq X ∖ (k ∖ u)$
78	77	difss2d	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (X ∖ (k ∖ u)) \subseteq X$
79		reldisj	$⊢ int (J) (X ∖ (k ∖ u)) \subseteq X \to (int (J) (X ∖ (k ∖ u)) \cap (k ∖ u) = \emptyset \leftrightarrow int (J) (X ∖ (k ∖ u)) \subseteq X ∖ (k ∖ u))$
80	78 79	syl	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to (int (J) (X ∖ (k ∖ u)) \cap (k ∖ u) = \emptyset \leftrightarrow int (J) (X ∖ (k ∖ u)) \subseteq X ∖ (k ∖ u))$
81	77 80	mpbird	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (X ∖ (k ∖ u)) \cap (k ∖ u) = \emptyset$
82		inssdif0	$⊢ int (J) (X ∖ (k ∖ u)) \cap k \subseteq u \leftrightarrow int (J) (X ∖ (k ∖ u)) \cap (k ∖ u) = \emptyset$
83	81 82	sylibr	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (X ∖ (k ∖ u)) \cap k \subseteq u$
84	75 83	sstrd	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \subseteq u$
85		eleq2	$⊢ z = int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \to (x \in z \leftrightarrow x \in (int (J) (X ∖ (k ∖ u)) \cap int (J) (k)))$
86		sseq1	$⊢ z = int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \to (z \subseteq u \leftrightarrow int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \subseteq u)$
87	85 86	anbi12d	$⊢ z = int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \to ((x \in z \land z \subseteq u) \leftrightarrow (x \in (int (J) (X ∖ (k ∖ u)) \cap int (J) (k)) \land int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \subseteq u))$
88	87	rspcev	$⊢ (int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \in J \land (x \in (int (J) (X ∖ (k ∖ u)) \cap int (J) (k)) \land int (J) (X ∖ (k ∖ u)) \cap int (J) (k) \subseteq u)) \to \exists z \in J (x \in z \land z \subseteq u)$
89	23 73 84 88	syl12anc	$⊢ (((φ \land u \in 𝑘Gen (J)) \land x \in u) \land (k \in nei (J) (\{x\}) \land J ↾_{𝑡} k \in Comp)) \to \exists z \in J (x \in z \land z \subseteq u)$
90	12 89	rexlimddv	$⊢ ((φ \land u \in 𝑘Gen (J)) \land x \in u) \to \exists z \in J (x \in z \land z \subseteq u)$
91	90	ralrimiva	$⊢ (φ \land u \in 𝑘Gen (J)) \to \forall x \in u \exists z \in J (x \in z \land z \subseteq u)$
92	91	ex	$⊢ φ \to (u \in 𝑘Gen (J) \to \forall x \in u \exists z \in J (x \in z \land z \subseteq u))$
93		eltop2	$⊢ J \in Top \to (u \in J \leftrightarrow \forall x \in u \exists z \in J (x \in z \land z \subseteq u))$
94	2 93	syl	$⊢ φ \to (u \in J \leftrightarrow \forall x \in u \exists z \in J (x \in z \land z \subseteq u))$
95	92 94	sylibrd	$⊢ φ \to (u \in 𝑘Gen (J) \to u \in J)$
96	95	ssrdv	$⊢ φ \to 𝑘Gen (J) \subseteq J$
97		iskgen2	$⊢ J \in ran 𝑘Gen \leftrightarrow (J \in Top \land 𝑘Gen (J) \subseteq J)$
98	2 96 97	sylanbrc	$⊢ φ \to J \in ran 𝑘Gen$

Metamath Proof Explorer

Theorem llycmpkgen2

Proof