2ndc1stc

Description: A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010)

		Ref	Expression
	Assertion	2ndc1stc	$⊢ J \in 2^{nd} 𝜔 \to J \in 1^{st} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		2ndctop	$⊢ J \in 2^{nd} 𝜔 \to J \in Top$
2		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists b \in TopBases (b ≼ ω \land topGen (b) = J)$
3		ssrab2	$⊢ \{q \in b \| x \in q\} \subseteq b$
4		bastg	$⊢ b \in TopBases \to b \subseteq topGen (b)$
5	4	3ad2ant1	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to b \subseteq topGen (b)$
6	3 5	sstrid	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to \{q \in b \| x \in q\} \subseteq topGen (b)$
7		fvex	$⊢ topGen (b) \in V$
8	7	elpw2	$⊢ \{q \in b \| x \in q\} \in 𝒫 topGen (b) \leftrightarrow \{q \in b \| x \in q\} \subseteq topGen (b)$
9	6 8	sylibr	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to \{q \in b \| x \in q\} \in 𝒫 topGen (b)$
10		vex	$⊢ b \in V$
11		ssdomg	$⊢ b \in V \to (\{q \in b \| x \in q\} \subseteq b \to \{q \in b \| x \in q\} ≼ b)$
12	10 3 11	mp2	$⊢ \{q \in b \| x \in q\} ≼ b$
13		simp2	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to b ≼ ω$
14		domtr	$⊢ (\{q \in b \| x \in q\} ≼ b \land b ≼ ω) \to \{q \in b \| x \in q\} ≼ ω$
15	12 13 14	sylancr	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to \{q \in b \| x \in q\} ≼ ω$
16		eltg2b	$⊢ b \in TopBases \to (o \in topGen (b) \leftrightarrow \forall y \in o \exists t \in b (y \in t \land t \subseteq o))$
17	16	3ad2ant1	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to (o \in topGen (b) \leftrightarrow \forall y \in o \exists t \in b (y \in t \land t \subseteq o))$
18		elequ1	$⊢ y = x \to (y \in t \leftrightarrow x \in t)$
19	18	anbi1d	$⊢ y = x \to ((y \in t \land t \subseteq o) \leftrightarrow (x \in t \land t \subseteq o))$
20	19	rexbidv	$⊢ y = x \to (\exists t \in b (y \in t \land t \subseteq o) \leftrightarrow \exists t \in b (x \in t \land t \subseteq o))$
21	20	rspccv	$⊢ \forall y \in o \exists t \in b (y \in t \land t \subseteq o) \to (x \in o \to \exists t \in b (x \in t \land t \subseteq o))$
22		id	$⊢ (t \in b \land x \in t) \to (t \in b \land x \in t)$
23	22	adantrr	$⊢ (t \in b \land (x \in t \land t \subseteq o)) \to (t \in b \land x \in t)$
24		elequ2	$⊢ q = t \to (x \in q \leftrightarrow x \in t)$
25	24	elrab	$⊢ t \in \{q \in b \| x \in q\} \leftrightarrow (t \in b \land x \in t)$
26	23 25	sylibr	$⊢ (t \in b \land (x \in t \land t \subseteq o)) \to t \in \{q \in b \| x \in q\}$
27		simprr	$⊢ ((b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \land (t \in b \land (x \in t \land t \subseteq o))) \to (x \in t \land t \subseteq o)$
28		elequ2	$⊢ p = t \to (x \in p \leftrightarrow x \in t)$
29		sseq1	$⊢ p = t \to (p \subseteq o \leftrightarrow t \subseteq o)$
30	28 29	anbi12d	$⊢ p = t \to ((x \in p \land p \subseteq o) \leftrightarrow (x \in t \land t \subseteq o))$
31	30	rspcev	$⊢ (t \in \{q \in b \| x \in q\} \land (x \in t \land t \subseteq o)) \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o)$
32	26 27 31	syl2an2	$⊢ ((b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \land (t \in b \land (x \in t \land t \subseteq o))) \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o)$
33	32	rexlimdvaa	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to (\exists t \in b (x \in t \land t \subseteq o) \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o))$
34	21 33	syl9r	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to (\forall y \in o \exists t \in b (y \in t \land t \subseteq o) \to (x \in o \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o)))$
35	17 34	sylbid	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to (o \in topGen (b) \to (x \in o \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o)))$
36	35	ralrimiv	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to \forall o \in topGen (b) (x \in o \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o))$
37		breq1	$⊢ s = \{q \in b \| x \in q\} \to (s ≼ ω \leftrightarrow \{q \in b \| x \in q\} ≼ ω)$
38		rexeq	$⊢ s = \{q \in b \| x \in q\} \to (\exists p \in s (x \in p \land p \subseteq o) \leftrightarrow \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o))$
39	38	imbi2d	$⊢ s = \{q \in b \| x \in q\} \to ((x \in o \to \exists p \in s (x \in p \land p \subseteq o)) \leftrightarrow (x \in o \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o)))$
40	39	ralbidv	$⊢ s = \{q \in b \| x \in q\} \to (\forall o \in topGen (b) (x \in o \to \exists p \in s (x \in p \land p \subseteq o)) \leftrightarrow \forall o \in topGen (b) (x \in o \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o)))$
41	37 40	anbi12d	$⊢ s = \{q \in b \| x \in q\} \to ((s ≼ ω \land \forall o \in topGen (b) (x \in o \to \exists p \in s (x \in p \land p \subseteq o))) \leftrightarrow (\{q \in b \| x \in q\} ≼ ω \land \forall o \in topGen (b) (x \in o \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o))))$
42	41	rspcev	$⊢ (\{q \in b \| x \in q\} \in 𝒫 topGen (b) \land (\{q \in b \| x \in q\} ≼ ω \land \forall o \in topGen (b) (x \in o \to \exists p \in \{q \in b \| x \in q\} (x \in p \land p \subseteq o)))) \to \exists s \in 𝒫 topGen (b) (s ≼ ω \land \forall o \in topGen (b) (x \in o \to \exists p \in s (x \in p \land p \subseteq o)))$
43	9 15 36 42	syl12anc	$⊢ (b \in TopBases \land b ≼ ω \land x \in ⋃ topGen (b)) \to \exists s \in 𝒫 topGen (b) (s ≼ ω \land \forall o \in topGen (b) (x \in o \to \exists p \in s (x \in p \land p \subseteq o)))$
44	43	3expia	$⊢ (b \in TopBases \land b ≼ ω) \to (x \in ⋃ topGen (b) \to \exists s \in 𝒫 topGen (b) (s ≼ ω \land \forall o \in topGen (b) (x \in o \to \exists p \in s (x \in p \land p \subseteq o))))$
45		unieq	$⊢ topGen (b) = J \to ⋃ topGen (b) = ⋃ J$
46	45	eleq2d	$⊢ topGen (b) = J \to (x \in ⋃ topGen (b) \leftrightarrow x \in ⋃ J)$
47		pweq	$⊢ topGen (b) = J \to 𝒫 topGen (b) = 𝒫 J$
48		raleq	$⊢ topGen (b) = J \to (\forall o \in topGen (b) (x \in o \to \exists p \in s (x \in p \land p \subseteq o)) \leftrightarrow \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o)))$
49	48	anbi2d	$⊢ topGen (b) = J \to ((s ≼ ω \land \forall o \in topGen (b) (x \in o \to \exists p \in s (x \in p \land p \subseteq o))) \leftrightarrow (s ≼ ω \land \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o))))$
50	47 49	rexeqbidv	$⊢ topGen (b) = J \to (\exists s \in 𝒫 topGen (b) (s ≼ ω \land \forall o \in topGen (b) (x \in o \to \exists p \in s (x \in p \land p \subseteq o))) \leftrightarrow \exists s \in 𝒫 J (s ≼ ω \land \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o))))$
51	46 50	imbi12d	$⊢ topGen (b) = J \to ((x \in ⋃ topGen (b) \to \exists s \in 𝒫 topGen (b) (s ≼ ω \land \forall o \in topGen (b) (x \in o \to \exists p \in s (x \in p \land p \subseteq o)))) \leftrightarrow (x \in ⋃ J \to \exists s \in 𝒫 J (s ≼ ω \land \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o)))))$
52	44 51	syl5ibcom	$⊢ (b \in TopBases \land b ≼ ω) \to (topGen (b) = J \to (x \in ⋃ J \to \exists s \in 𝒫 J (s ≼ ω \land \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o)))))$
53	52	expimpd	$⊢ b \in TopBases \to ((b ≼ ω \land topGen (b) = J) \to (x \in ⋃ J \to \exists s \in 𝒫 J (s ≼ ω \land \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o)))))$
54	53	rexlimiv	$⊢ \exists b \in TopBases (b ≼ ω \land topGen (b) = J) \to (x \in ⋃ J \to \exists s \in 𝒫 J (s ≼ ω \land \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o))))$
55	2 54	sylbi	$⊢ J \in 2^{nd} 𝜔 \to (x \in ⋃ J \to \exists s \in 𝒫 J (s ≼ ω \land \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o))))$
56	55	ralrimiv	$⊢ J \in 2^{nd} 𝜔 \to \forall x \in ⋃ J \exists s \in 𝒫 J (s ≼ ω \land \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o)))$
57		eqid	$⊢ ⋃ J = ⋃ J$
58	57	is1stc2	$⊢ J \in 1^{st} 𝜔 \leftrightarrow (J \in Top \land \forall x \in ⋃ J \exists s \in 𝒫 J (s ≼ ω \land \forall o \in J (x \in o \to \exists p \in s (x \in p \land p \subseteq o))))$
59	1 56 58	sylanbrc	$⊢ J \in 2^{nd} 𝜔 \to J \in 1^{st} 𝜔$

Metamath Proof Explorer

Theorem 2ndc1stc

Proof