2ndcsep

Description: A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015)

		Ref	Expression
	Hypothesis	2ndcsep.1	$⊢ X = ⋃ J$
	Assertion	2ndcsep	$⊢ J \in 2^{nd} 𝜔 \to \exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X)$

Proof

Step	Hyp	Ref	Expression
1		2ndcsep.1	$⊢ X = ⋃ J$
2		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists b \in TopBases (b ≼ ω \land topGen (b) = J)$
3		vex	$⊢ b \in V$
4		difss	$⊢ b ∖ \{\emptyset\} \subseteq b$
5		ssdomg	$⊢ b \in V \to (b ∖ \{\emptyset\} \subseteq b \to (b ∖ \{\emptyset\}) ≼ b)$
6	3 4 5	mp2	$⊢ (b ∖ \{\emptyset\}) ≼ b$
7		simpr	$⊢ (b \in TopBases \land b ≼ ω) \to b ≼ ω$
8		domtr	$⊢ ((b ∖ \{\emptyset\}) ≼ b \land b ≼ ω) \to (b ∖ \{\emptyset\}) ≼ ω$
9	6 7 8	sylancr	$⊢ (b \in TopBases \land b ≼ ω) \to (b ∖ \{\emptyset\}) ≼ ω$
10		eldifsn	$⊢ y \in (b ∖ \{\emptyset\}) \leftrightarrow (y \in b \land y \neq \emptyset)$
11		n0	$⊢ y \neq \emptyset \leftrightarrow \exists z z \in y$
12		elunii	$⊢ (z \in y \land y \in b) \to z \in ⋃ b$
13		simpl	$⊢ (z \in y \land y \in b) \to z \in y$
14	12 13	jca	$⊢ (z \in y \land y \in b) \to (z \in ⋃ b \land z \in y)$
15	14	expcom	$⊢ y \in b \to (z \in y \to (z \in ⋃ b \land z \in y))$
16	15	eximdv	$⊢ y \in b \to (\exists z z \in y \to \exists z (z \in ⋃ b \land z \in y))$
17	16	imp	$⊢ (y \in b \land \exists z z \in y) \to \exists z (z \in ⋃ b \land z \in y)$
18		df-rex	$⊢ \exists z \in ⋃ b z \in y \leftrightarrow \exists z (z \in ⋃ b \land z \in y)$
19	17 18	sylibr	$⊢ (y \in b \land \exists z z \in y) \to \exists z \in ⋃ b z \in y$
20	11 19	sylan2b	$⊢ (y \in b \land y \neq \emptyset) \to \exists z \in ⋃ b z \in y$
21	10 20	sylbi	$⊢ y \in (b ∖ \{\emptyset\}) \to \exists z \in ⋃ b z \in y$
22	21	rgen	$⊢ \forall y \in (b ∖ \{\emptyset\}) \exists z \in ⋃ b z \in y$
23		vuniex	$⊢ ⋃ b \in V$
24		eleq1	$⊢ z = f (y) \to (z \in y \leftrightarrow f (y) \in y)$
25	23 24	axcc4dom	$⊢ ((b ∖ \{\emptyset\}) ≼ ω \land \forall y \in (b ∖ \{\emptyset\}) \exists z \in ⋃ b z \in y) \to \exists f (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)$
26	9 22 25	sylancl	$⊢ (b \in TopBases \land b ≼ ω) \to \exists f (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)$
27		frn	$⊢ f : b ∖ \{\emptyset\} ⟶ ⋃ b \to ran f \subseteq ⋃ b$
28	27	ad2antrl	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to ran f \subseteq ⋃ b$
29		vex	$⊢ f \in V$
30	29	rnex	$⊢ ran f \in V$
31	30	elpw	$⊢ ran f \in 𝒫 ⋃ b \leftrightarrow ran f \subseteq ⋃ b$
32	28 31	sylibr	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to ran f \in 𝒫 ⋃ b$
33		omelon	$⊢ ω \in On$
34	7	adantr	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to b ≼ ω$
35		ondomen	$⊢ (ω \in On \land b ≼ ω) \to b \in dom card$
36	33 34 35	sylancr	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to b \in dom card$
37		ssnum	$⊢ (b \in dom card \land b ∖ \{\emptyset\} \subseteq b) \to b ∖ \{\emptyset\} \in dom card$
38	36 4 37	sylancl	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to b ∖ \{\emptyset\} \in dom card$
39		ffn	$⊢ f : b ∖ \{\emptyset\} ⟶ ⋃ b \to f Fn (b ∖ \{\emptyset\})$
40	39	ad2antrl	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to f Fn (b ∖ \{\emptyset\})$
41		dffn4	$⊢ f Fn (b ∖ \{\emptyset\}) \leftrightarrow f : b ∖ \{\emptyset\} \underset{onto}{⟶} ran f$
42	40 41	sylib	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to f : b ∖ \{\emptyset\} \underset{onto}{⟶} ran f$
43		fodomnum	$⊢ b ∖ \{\emptyset\} \in dom card \to (f : b ∖ \{\emptyset\} \underset{onto}{⟶} ran f \to ran f ≼ (b ∖ \{\emptyset\}))$
44	38 42 43	sylc	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to ran f ≼ (b ∖ \{\emptyset\})$
45	9	adantr	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to (b ∖ \{\emptyset\}) ≼ ω$
46		domtr	$⊢ (ran f ≼ (b ∖ \{\emptyset\}) \land (b ∖ \{\emptyset\}) ≼ ω) \to ran f ≼ ω$
47	44 45 46	syl2anc	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to ran f ≼ ω$
48		tgcl	$⊢ b \in TopBases \to topGen (b) \in Top$
49	48	ad2antrr	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to topGen (b) \in Top$
50		unitg	$⊢ b \in V \to ⋃ topGen (b) = ⋃ b$
51	50	elv	$⊢ ⋃ topGen (b) = ⋃ b$
52	51	eqcomi	$⊢ ⋃ b = ⋃ topGen (b)$
53	52	clsss3	$⊢ (topGen (b) \in Top \land ran f \subseteq ⋃ b) \to cls (topGen (b)) (ran f) \subseteq ⋃ b$
54	49 28 53	syl2anc	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to cls (topGen (b)) (ran f) \subseteq ⋃ b$
55		ne0i	$⊢ x \in y \to y \neq \emptyset$
56	55	anim2i	$⊢ (y \in b \land x \in y) \to (y \in b \land y \neq \emptyset)$
57	56 10	sylibr	$⊢ (y \in b \land x \in y) \to y \in (b ∖ \{\emptyset\})$
58		fnfvelrn	$⊢ (f Fn (b ∖ \{\emptyset\}) \land y \in (b ∖ \{\emptyset\})) \to f (y) \in ran f$
59	39 58	sylan	$⊢ (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land y \in (b ∖ \{\emptyset\})) \to f (y) \in ran f$
60		inelcm	$⊢ (f (y) \in y \land f (y) \in ran f) \to y \cap ran f \neq \emptyset$
61	60	expcom	$⊢ f (y) \in ran f \to (f (y) \in y \to y \cap ran f \neq \emptyset)$
62	59 61	syl	$⊢ (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land y \in (b ∖ \{\emptyset\})) \to (f (y) \in y \to y \cap ran f \neq \emptyset)$
63	62	ex	$⊢ f : b ∖ \{\emptyset\} ⟶ ⋃ b \to (y \in (b ∖ \{\emptyset\}) \to (f (y) \in y \to y \cap ran f \neq \emptyset))$
64	63	a2d	$⊢ f : b ∖ \{\emptyset\} ⟶ ⋃ b \to ((y \in (b ∖ \{\emptyset\}) \to f (y) \in y) \to (y \in (b ∖ \{\emptyset\}) \to y \cap ran f \neq \emptyset))$
65	57 64	syl7	$⊢ f : b ∖ \{\emptyset\} ⟶ ⋃ b \to ((y \in (b ∖ \{\emptyset\}) \to f (y) \in y) \to ((y \in b \land x \in y) \to y \cap ran f \neq \emptyset))$
66	65	exp4a	$⊢ f : b ∖ \{\emptyset\} ⟶ ⋃ b \to ((y \in (b ∖ \{\emptyset\}) \to f (y) \in y) \to (y \in b \to (x \in y \to y \cap ran f \neq \emptyset)))$
67	66	ralimdv2	$⊢ f : b ∖ \{\emptyset\} ⟶ ⋃ b \to (\forall y \in (b ∖ \{\emptyset\}) f (y) \in y \to \forall y \in b (x \in y \to y \cap ran f \neq \emptyset))$
68	67	imp	$⊢ (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y) \to \forall y \in b (x \in y \to y \cap ran f \neq \emptyset)$
69	68	ad2antlr	$⊢ (((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \land x \in ⋃ b) \to \forall y \in b (x \in y \to y \cap ran f \neq \emptyset)$
70		eqidd	$⊢ (((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \land x \in ⋃ b) \to topGen (b) = topGen (b)$
71	52	a1i	$⊢ (((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \land x \in ⋃ b) \to ⋃ b = ⋃ topGen (b)$
72		simplll	$⊢ (((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \land x \in ⋃ b) \to b \in TopBases$
73	28	adantr	$⊢ (((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \land x \in ⋃ b) \to ran f \subseteq ⋃ b$
74		simpr	$⊢ (((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \land x \in ⋃ b) \to x \in ⋃ b$
75	70 71 72 73 74	elcls3	$⊢ (((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \land x \in ⋃ b) \to (x \in cls (topGen (b)) (ran f) \leftrightarrow \forall y \in b (x \in y \to y \cap ran f \neq \emptyset))$
76	69 75	mpbird	$⊢ (((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \land x \in ⋃ b) \to x \in cls (topGen (b)) (ran f)$
77	54 76	eqelssd	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to cls (topGen (b)) (ran f) = ⋃ b$
78		breq1	$⊢ x = ran f \to (x ≼ ω \leftrightarrow ran f ≼ ω)$
79		fveqeq2	$⊢ x = ran f \to (cls (topGen (b)) (x) = ⋃ b \leftrightarrow cls (topGen (b)) (ran f) = ⋃ b)$
80	78 79	anbi12d	$⊢ x = ran f \to ((x ≼ ω \land cls (topGen (b)) (x) = ⋃ b) \leftrightarrow (ran f ≼ ω \land cls (topGen (b)) (ran f) = ⋃ b))$
81	80	rspcev	$⊢ (ran f \in 𝒫 ⋃ b \land (ran f ≼ ω \land cls (topGen (b)) (ran f) = ⋃ b)) \to \exists x \in 𝒫 ⋃ b (x ≼ ω \land cls (topGen (b)) (x) = ⋃ b)$
82	32 47 77 81	syl12anc	$⊢ ((b \in TopBases \land b ≼ ω) \land (f : b ∖ \{\emptyset\} ⟶ ⋃ b \land \forall y \in (b ∖ \{\emptyset\}) f (y) \in y)) \to \exists x \in 𝒫 ⋃ b (x ≼ ω \land cls (topGen (b)) (x) = ⋃ b)$
83	26 82	exlimddv	$⊢ (b \in TopBases \land b ≼ ω) \to \exists x \in 𝒫 ⋃ b (x ≼ ω \land cls (topGen (b)) (x) = ⋃ b)$
84		unieq	$⊢ topGen (b) = J \to ⋃ topGen (b) = ⋃ J$
85	84 52 1	3eqtr4g	$⊢ topGen (b) = J \to ⋃ b = X$
86	85	pweqd	$⊢ topGen (b) = J \to 𝒫 ⋃ b = 𝒫 X$
87		fveq2	$⊢ topGen (b) = J \to cls (topGen (b)) = cls (J)$
88	87	fveq1d	$⊢ topGen (b) = J \to cls (topGen (b)) (x) = cls (J) (x)$
89	88 85	eqeq12d	$⊢ topGen (b) = J \to (cls (topGen (b)) (x) = ⋃ b \leftrightarrow cls (J) (x) = X)$
90	89	anbi2d	$⊢ topGen (b) = J \to ((x ≼ ω \land cls (topGen (b)) (x) = ⋃ b) \leftrightarrow (x ≼ ω \land cls (J) (x) = X))$
91	86 90	rexeqbidv	$⊢ topGen (b) = J \to (\exists x \in 𝒫 ⋃ b (x ≼ ω \land cls (topGen (b)) (x) = ⋃ b) \leftrightarrow \exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X))$
92	83 91	syl5ibcom	$⊢ (b \in TopBases \land b ≼ ω) \to (topGen (b) = J \to \exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X))$
93	92	impr	$⊢ (b \in TopBases \land (b ≼ ω \land topGen (b) = J)) \to \exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X)$
94	93	rexlimiva	$⊢ \exists b \in TopBases (b ≼ ω \land topGen (b) = J) \to \exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X)$
95	2 94	sylbi	$⊢ J \in 2^{nd} 𝜔 \to \exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X)$

Metamath Proof Explorer

Theorem 2ndcsep

Proof