2ndcsb

Description: Having a countable subbase is a sufficient condition for second-countability. (Contributed by Jeff Hankins, 17-Jan-2010) (Proof shortened by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	2ndcsb	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists x (x ≼ ω \land topGen (fi (x)) = J)$

Proof

Step	Hyp	Ref	Expression
1		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists x \in TopBases (x ≼ ω \land topGen (x) = J)$
2		df-rex	$⊢ \exists x \in TopBases (x ≼ ω \land topGen (x) = J) \leftrightarrow \exists x (x \in TopBases \land (x ≼ ω \land topGen (x) = J))$
3		simprl	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to x ≼ ω$
4		ssfii	$⊢ x \in TopBases \to x \subseteq fi (x)$
5		fvex	$⊢ topGen (x) \in V$
6		bastg	$⊢ x \in TopBases \to x \subseteq topGen (x)$
7	6	adantr	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to x \subseteq topGen (x)$
8		fiss	$⊢ (topGen (x) \in V \land x \subseteq topGen (x)) \to fi (x) \subseteq fi (topGen (x))$
9	5 7 8	sylancr	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to fi (x) \subseteq fi (topGen (x))$
10		tgcl	$⊢ x \in TopBases \to topGen (x) \in Top$
11	10	adantr	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to topGen (x) \in Top$
12		fitop	$⊢ topGen (x) \in Top \to fi (topGen (x)) = topGen (x)$
13	11 12	syl	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to fi (topGen (x)) = topGen (x)$
14	9 13	sseqtrd	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to fi (x) \subseteq topGen (x)$
15		2basgen	$⊢ (x \subseteq fi (x) \land fi (x) \subseteq topGen (x)) \to topGen (x) = topGen (fi (x))$
16	4 14 15	syl2an2r	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to topGen (x) = topGen (fi (x))$
17		simprr	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to topGen (x) = J$
18	16 17	eqtr3d	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to topGen (fi (x)) = J$
19	3 18	jca	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to (x ≼ ω \land topGen (fi (x)) = J)$
20	19	eximi	$⊢ \exists x (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to \exists x (x ≼ ω \land topGen (fi (x)) = J)$
21	2 20	sylbi	$⊢ \exists x \in TopBases (x ≼ ω \land topGen (x) = J) \to \exists x (x ≼ ω \land topGen (fi (x)) = J)$
22	1 21	sylbi	$⊢ J \in 2^{nd} 𝜔 \to \exists x (x ≼ ω \land topGen (fi (x)) = J)$
23		fibas	$⊢ fi (x) \in TopBases$
24		simpl	$⊢ (x ≼ ω \land topGen (fi (x)) = J) \to x ≼ ω$
25		fictb	$⊢ x \in V \to (x ≼ ω \leftrightarrow fi (x) ≼ ω)$
26	25	elv	$⊢ x ≼ ω \leftrightarrow fi (x) ≼ ω$
27	24 26	sylib	$⊢ (x ≼ ω \land topGen (fi (x)) = J) \to fi (x) ≼ ω$
28		simpr	$⊢ (x ≼ ω \land topGen (fi (x)) = J) \to topGen (fi (x)) = J$
29	27 28	jca	$⊢ (x ≼ ω \land topGen (fi (x)) = J) \to (fi (x) ≼ ω \land topGen (fi (x)) = J)$
30		breq1	$⊢ y = fi (x) \to (y ≼ ω \leftrightarrow fi (x) ≼ ω)$
31		fveqeq2	$⊢ y = fi (x) \to (topGen (y) = J \leftrightarrow topGen (fi (x)) = J)$
32	30 31	anbi12d	$⊢ y = fi (x) \to ((y ≼ ω \land topGen (y) = J) \leftrightarrow (fi (x) ≼ ω \land topGen (fi (x)) = J))$
33	32	rspcev	$⊢ (fi (x) \in TopBases \land (fi (x) ≼ ω \land topGen (fi (x)) = J)) \to \exists y \in TopBases (y ≼ ω \land topGen (y) = J)$
34	23 29 33	sylancr	$⊢ (x ≼ ω \land topGen (fi (x)) = J) \to \exists y \in TopBases (y ≼ ω \land topGen (y) = J)$
35		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists y \in TopBases (y ≼ ω \land topGen (y) = J)$
36	34 35	sylibr	$⊢ (x ≼ ω \land topGen (fi (x)) = J) \to J \in 2^{nd} 𝜔$
37	36	exlimiv	$⊢ \exists x (x ≼ ω \land topGen (fi (x)) = J) \to J \in 2^{nd} 𝜔$
38	22 37	impbii	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists x (x ≼ ω \land topGen (fi (x)) = J)$

Metamath Proof Explorer

Theorem 2ndcsb

Proof