1stckgen

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

		Ref	Expression
	Assertion	1stckgen	$⊢ J \in 1^{st} 𝜔 \to J \in ran 𝑘Gen$

Proof

Step	Hyp	Ref	Expression
1		1stctop	$⊢ J \in 1^{st} 𝜔 \to J \in Top$
2		difss	$⊢ ⋃ J ∖ x \subseteq ⋃ J$
3		eqid	$⊢ ⋃ J = ⋃ J$
4	3	1stcelcls	$⊢ (J \in 1^{st} 𝜔 \land ⋃ J ∖ x \subseteq ⋃ J) \to (y \in cls (J) (⋃ J ∖ x) \leftrightarrow \exists f (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y))$
5	2 4	mpan2	$⊢ J \in 1^{st} 𝜔 \to (y \in cls (J) (⋃ J ∖ x) \leftrightarrow \exists f (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y))$
6	5	adantr	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to (y \in cls (J) (⋃ J ∖ x) \leftrightarrow \exists f (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y))$
7	1	adantr	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to J \in Top$
8	7	adantr	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to J \in Top$
9		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
10	8 9	sylib	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to J \in TopOn (⋃ J)$
11		simprr	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to f \underset{t}{⇝} (J) y$
12		lmcl	$⊢ (J \in TopOn (⋃ J) \land f \underset{t}{⇝} (J) y) \to y \in ⋃ J$
13	10 11 12	syl2anc	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to y \in ⋃ J$
14		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
15		vex	$⊢ f \in V$
16	15	rnex	$⊢ ran f \in V$
17		vsnex	$⊢ \{y\} \in V$
18	16 17	unex	$⊢ ran f \cup \{y\} \in V$
19		resttop	$⊢ (J \in Top \land ran f \cup \{y\} \in V) \to J ↾_{𝑡} (ran f \cup \{y\}) \in Top$
20	8 18 19	sylancl	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to J ↾_{𝑡} (ran f \cup \{y\}) \in Top$
21		toptopon2	$⊢ J ↾_{𝑡} (ran f \cup \{y\}) \in Top \leftrightarrow J ↾_{𝑡} (ran f \cup \{y\}) \in TopOn (⋃ (J ↾_{𝑡} (ran f \cup \{y\})))$
22	20 21	sylib	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to J ↾_{𝑡} (ran f \cup \{y\}) \in TopOn (⋃ (J ↾_{𝑡} (ran f \cup \{y\})))$
23		1zzd	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to 1 \in ℤ$
24		eqid	$⊢ J ↾_{𝑡} (ran f \cup \{y\}) = J ↾_{𝑡} (ran f \cup \{y\})$
25	18	a1i	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to ran f \cup \{y\} \in V$
26		ssun2	$⊢ \{y\} \subseteq ran f \cup \{y\}$
27		vex	$⊢ y \in V$
28	27	snss	$⊢ y \in (ran f \cup \{y\}) \leftrightarrow \{y\} \subseteq ran f \cup \{y\}$
29	26 28	mpbir	$⊢ y \in (ran f \cup \{y\})$
30	29	a1i	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to y \in (ran f \cup \{y\})$
31		ffn	$⊢ f : ℕ ⟶ ⋃ J ∖ x \to f Fn ℕ$
32	31	ad2antrl	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to f Fn ℕ$
33		dffn3	$⊢ f Fn ℕ \leftrightarrow f : ℕ ⟶ ran f$
34	32 33	sylib	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to f : ℕ ⟶ ran f$
35		ssun1	$⊢ ran f \subseteq ran f \cup \{y\}$
36		fss	$⊢ (f : ℕ ⟶ ran f \land ran f \subseteq ran f \cup \{y\}) \to f : ℕ ⟶ ran f \cup \{y\}$
37	34 35 36	sylancl	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to f : ℕ ⟶ ran f \cup \{y\}$
38	24 14 25 8 30 23 37	lmss	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to (f \underset{t}{⇝} (J) y \leftrightarrow f \underset{t}{⇝} (J ↾_{𝑡} (ran f \cup \{y\})) y)$
39	11 38	mpbid	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to f \underset{t}{⇝} (J ↾_{𝑡} (ran f \cup \{y\})) y$
40	37	ffvelcdmda	$⊢ (((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \land k \in ℕ) \to f (k) \in (ran f \cup \{y\})$
41		simprl	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to f : ℕ ⟶ ⋃ J ∖ x$
42	41	ffvelcdmda	$⊢ (((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \land k \in ℕ) \to f (k) \in (⋃ J ∖ x)$
43	42	eldifbd	$⊢ (((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \land k \in ℕ) \to \neg f (k) \in x$
44	40 43	eldifd	$⊢ (((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \land k \in ℕ) \to f (k) \in ((ran f \cup \{y\}) ∖ x)$
45		difin	$⊢ (ran f \cup \{y\}) ∖ ((ran f \cup \{y\}) \cap x) = (ran f \cup \{y\}) ∖ x$
46		frn	$⊢ f : ℕ ⟶ ⋃ J ∖ x \to ran f \subseteq ⋃ J ∖ x$
47	46	ad2antrl	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to ran f \subseteq ⋃ J ∖ x$
48	47	difss2d	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to ran f \subseteq ⋃ J$
49	13	snssd	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to \{y\} \subseteq ⋃ J$
50	48 49	unssd	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to ran f \cup \{y\} \subseteq ⋃ J$
51	3	restuni	$⊢ (J \in Top \land ran f \cup \{y\} \subseteq ⋃ J) \to ran f \cup \{y\} = ⋃ (J ↾_{𝑡} (ran f \cup \{y\}))$
52	8 50 51	syl2anc	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to ran f \cup \{y\} = ⋃ (J ↾_{𝑡} (ran f \cup \{y\}))$
53	52	difeq1d	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to (ran f \cup \{y\}) ∖ ((ran f \cup \{y\}) \cap x) = ⋃ (J ↾_{𝑡} (ran f \cup \{y\})) ∖ ((ran f \cup \{y\}) \cap x)$
54	45 53	eqtr3id	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to (ran f \cup \{y\}) ∖ x = ⋃ (J ↾_{𝑡} (ran f \cup \{y\})) ∖ ((ran f \cup \{y\}) \cap x)$
55		incom	$⊢ (ran f \cup \{y\}) \cap x = x \cap (ran f \cup \{y\})$
56		simplr	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to x \in 𝑘Gen (J)$
57		fss	$⊢ (f : ℕ ⟶ ⋃ J ∖ x \land ⋃ J ∖ x \subseteq ⋃ J) \to f : ℕ ⟶ ⋃ J$
58	41 2 57	sylancl	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to f : ℕ ⟶ ⋃ J$
59	10 58 11	1stckgenlem	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to J ↾_{𝑡} (ran f \cup \{y\}) \in Comp$
60		kgeni	$⊢ (x \in 𝑘Gen (J) \land J ↾_{𝑡} (ran f \cup \{y\}) \in Comp) \to x \cap (ran f \cup \{y\}) \in (J ↾_{𝑡} (ran f \cup \{y\}))$
61	56 59 60	syl2anc	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to x \cap (ran f \cup \{y\}) \in (J ↾_{𝑡} (ran f \cup \{y\}))$
62	55 61	eqeltrid	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to (ran f \cup \{y\}) \cap x \in (J ↾_{𝑡} (ran f \cup \{y\}))$
63		eqid	$⊢ ⋃ (J ↾_{𝑡} (ran f \cup \{y\})) = ⋃ (J ↾_{𝑡} (ran f \cup \{y\}))$
64	63	opncld	$⊢ (J ↾_{𝑡} (ran f \cup \{y\}) \in Top \land (ran f \cup \{y\}) \cap x \in (J ↾_{𝑡} (ran f \cup \{y\}))) \to ⋃ (J ↾_{𝑡} (ran f \cup \{y\})) ∖ ((ran f \cup \{y\}) \cap x) \in Clsd (J ↾_{𝑡} (ran f \cup \{y\}))$
65	20 62 64	syl2anc	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to ⋃ (J ↾_{𝑡} (ran f \cup \{y\})) ∖ ((ran f \cup \{y\}) \cap x) \in Clsd (J ↾_{𝑡} (ran f \cup \{y\}))$
66	54 65	eqeltrd	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to (ran f \cup \{y\}) ∖ x \in Clsd (J ↾_{𝑡} (ran f \cup \{y\}))$
67	14 22 23 39 44 66	lmcld	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to y \in ((ran f \cup \{y\}) ∖ x)$
68	67	eldifbd	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to \neg y \in x$
69	13 68	eldifd	$⊢ ((J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \land (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y)) \to y \in (⋃ J ∖ x)$
70	69	ex	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to ((f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y) \to y \in (⋃ J ∖ x))$
71	70	exlimdv	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to (\exists f (f : ℕ ⟶ ⋃ J ∖ x \land f \underset{t}{⇝} (J) y) \to y \in (⋃ J ∖ x))$
72	6 71	sylbid	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to (y \in cls (J) (⋃ J ∖ x) \to y \in (⋃ J ∖ x))$
73	72	ssrdv	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to cls (J) (⋃ J ∖ x) \subseteq ⋃ J ∖ x$
74	3	iscld4	$⊢ (J \in Top \land ⋃ J ∖ x \subseteq ⋃ J) \to (⋃ J ∖ x \in Clsd (J) \leftrightarrow cls (J) (⋃ J ∖ x) \subseteq ⋃ J ∖ x)$
75	7 2 74	sylancl	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to (⋃ J ∖ x \in Clsd (J) \leftrightarrow cls (J) (⋃ J ∖ x) \subseteq ⋃ J ∖ x)$
76	73 75	mpbird	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to ⋃ J ∖ x \in Clsd (J)$
77		elssuni	$⊢ x \in 𝑘Gen (J) \to x \subseteq ⋃ 𝑘Gen (J)$
78	77	adantl	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to x \subseteq ⋃ 𝑘Gen (J)$
79	3	kgenuni	$⊢ J \in Top \to ⋃ J = ⋃ 𝑘Gen (J)$
80	7 79	syl	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to ⋃ J = ⋃ 𝑘Gen (J)$
81	78 80	sseqtrrd	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to x \subseteq ⋃ J$
82	3	isopn2	$⊢ (J \in Top \land x \subseteq ⋃ J) \to (x \in J \leftrightarrow ⋃ J ∖ x \in Clsd (J))$
83	7 81 82	syl2anc	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to (x \in J \leftrightarrow ⋃ J ∖ x \in Clsd (J))$
84	76 83	mpbird	$⊢ (J \in 1^{st} 𝜔 \land x \in 𝑘Gen (J)) \to x \in J$
85	84	ex	$⊢ J \in 1^{st} 𝜔 \to (x \in 𝑘Gen (J) \to x \in J)$
86	85	ssrdv	$⊢ J \in 1^{st} 𝜔 \to 𝑘Gen (J) \subseteq J$
87		iskgen2	$⊢ J \in ran 𝑘Gen \leftrightarrow (J \in Top \land 𝑘Gen (J) \subseteq J)$
88	1 86 87	sylanbrc	$⊢ J \in 1^{st} 𝜔 \to J \in ran 𝑘Gen$

Metamath Proof Explorer

Theorem 1stckgen

Proof