Theorem 2ndc1stc 15477

Description: A second-countable space is first-countable.

Assertion

Ref	Expression
2ndc1stc	|- (J e. 2ndc -> J e. 1stc)

Proof of Theorem 2ndc1stc

Step	Hyp	Ref	Expression
1		is2ndc2 15473	. . . 4 |- (J e. 2ndc <-> E.b e. Bases (b ~<_ om /\ (topGen` b) = J))
2		unieq 3185	. . . . . . . . 9 |- ((topGen` b) = J -> U.(topGen` b) = U.J)
3	2	eleq2d 1964	. . . . . . . 8 |- ((topGen` b) = J -> (x e. U.(topGen` b) <-> x e. U.J))
4		pweq 3036	. . . . . . . . 9 |- ((topGen` b) = J -> ~P(topGen` b) = ~PJ)
5		raleq 2266	. . . . . . . . . 10 |- ((topGen` b) = J -> (A.o e. (topGen` b)(x e. o -> E.p e. s (x e. p /\ p C_ o)) <-> A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o))))
6	5	anbi2d 678	. . . . . . . . 9 |- ((topGen` b) = J -> ((s ~<_ om /\ A.o e. (topGen` b)(x e. o -> E.p e. s (x e. p /\ p C_ o))) <-> (s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o)))))
7	4, 6	rexeqbidv 2275	. . . . . . . 8 |- ((topGen` b) = J -> (E.s e. ~P (topGen` b)(s ~<_ om /\ A.o e. (topGen` b)(x e. o -> E.p e. s (x e. p /\ p C_ o))) <-> E.s e. ~P J(s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o)))))
8	3, 7	imbi12d 688	. . . . . . 7 |- ((topGen` b) = J -> ((x e. U.(topGen` b) -> E.s e. ~P (topGen` b)(s ~<_ om /\ A.o e. (topGen` b)(x e. o -> E.p e. s (x e. p /\ p C_ o)))) <-> (x e. U.J -> E.s e. ~P J(s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o))))))
9		ssrab2 2692	. . . . . . . . . . . 12 |- {q e. b | x e. q} C_ b
10	9	a1i 8	. . . . . . . . . . 11 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> {q e. b | x e. q} C_ b)
11		bastg 8892	. . . . . . . . . . . 12 |- (b e. Bases -> b C_ (topGen` b))
12	11	3ad2ant1 897	. . . . . . . . . . 11 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> b C_ (topGen` b))
13	10, 12	sstrd 2627	. . . . . . . . . 10 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> {q e. b | x e. q} C_ (topGen` b))
14		fvex 4689	. . . . . . . . . . 11 |- (topGen` b) e. _V
15	14	elpw2 3464	. . . . . . . . . 10 |- ({q e. b | x e. q} e. ~P(topGen` b) <-> {q e. b | x e. q} C_ (topGen` b))
16	13, 15	sylibr 217	. . . . . . . . 9 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> {q e. b | x e. q} e. ~P(topGen` b))
17		visset 2295	. . . . . . . . . . . . 13 |- b e. _V
18	17	rabex 3461	. . . . . . . . . . . 12 |- {q e. b | x e. q} e. _V
19		ssdomg 5467	. . . . . . . . . . . 12 |- ({q e. b | x e. q} e. _V -> ({q e. b | x e. q} C_ b -> {q e. b | x e. q} ~<_ b))
20	18, 9, 19	mp2 54	. . . . . . . . . . 11 |- {q e. b | x e. q} ~<_ b
21	20	a1i 8	. . . . . . . . . 10 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> {q e. b | x e. q} ~<_ b)
22		simp2 877	. . . . . . . . . 10 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> b ~<_ om)
23		domtr 5474	. . . . . . . . . 10 |- (({q e. b | x e. q} ~<_ b /\ b ~<_ om) -> {q e. b | x e. q} ~<_ om)
24	21, 22, 23	syl11anc 524	. . . . . . . . 9 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> {q e. b | x e. q} ~<_ om)
25		eltg2 8889	. . . . . . . . . . . 12 |- (b e. Bases -> (o e. (topGen` b) <-> (o C_ U.b /\ A.y e. o E.t e. b (y e. t /\ t C_ o))))
26	25	3ad2ant1 897	. . . . . . . . . . 11 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> (o e. (topGen` b) <-> (o C_ U.b /\ A.y e. o E.t e. b (y e. t /\ t C_ o))))
27		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (y = x -> (y e. t <-> x e. t))
28	27	anbi1d 679	. . . . . . . . . . . . . . 15 |- (y = x -> ((y e. t /\ t C_ o) <-> (x e. t /\ t C_ o)))
29	28	rexbidv 2124	. . . . . . . . . . . . . 14 |- (y = x -> (E.t e. b (y e. t /\ t C_ o) <-> E.t e. b (x e. t /\ t C_ o)))
30	29	rcla4cv 2377	. . . . . . . . . . . . 13 |- (A.y e. o E.t e. b (y e. t /\ t C_ o) -> (x e. o -> E.t e. b (x e. t /\ t C_ o)))
31		id 73	. . . . . . . . . . . . . . . . . . 19 |- ((t e. b /\ x e. t) -> (t e. b /\ x e. t))
32	31	adantrr 431	. . . . . . . . . . . . . . . . . 18 |- ((t e. b /\ (x e. t /\ t C_ o)) -> (t e. b /\ x e. t))
33		eleq2 1958	. . . . . . . . . . . . . . . . . . 19 |- (q = t -> (x e. q <-> x e. t))
34	33	elrab 2414	. . . . . . . . . . . . . . . . . 18 |- (t e. {q e. b | x e. q} <-> (t e. b /\ x e. t))
35	32, 34	sylibr 217	. . . . . . . . . . . . . . . . 17 |- ((t e. b /\ (x e. t /\ t C_ o)) -> t e. {q e. b | x e. q})
36	35	adantl 424	. . . . . . . . . . . . . . . 16 |- (((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) /\ (t e. b /\ (x e. t /\ t C_ o))) -> t e. {q e. b | x e. q})
37		simprr 451	. . . . . . . . . . . . . . . 16 |- (((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) /\ (t e. b /\ (x e. t /\ t C_ o))) -> (x e. t /\ t C_ o))
38		eleq2 1958	. . . . . . . . . . . . . . . . . 18 |- (p = t -> (x e. p <-> x e. t))
39		sseq1 2637	. . . . . . . . . . . . . . . . . 18 |- (p = t -> (p C_ o <-> t C_ o))
40	38, 39	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (p = t -> ((x e. p /\ p C_ o) <-> (x e. t /\ t C_ o)))
41	40	rcla4ev 2381	. . . . . . . . . . . . . . . 16 |- ((t e. {q e. b | x e. q} /\ (x e. t /\ t C_ o)) -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o))
42	36, 37, 41	syl11anc 524	. . . . . . . . . . . . . . 15 |- (((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) /\ (t e. b /\ (x e. t /\ t C_ o))) -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o))
43	42	exp32 408	. . . . . . . . . . . . . 14 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> (t e. b -> ((x e. t /\ t C_ o) -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o))))
44	43	r19.23adv 2215	. . . . . . . . . . . . 13 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> (E.t e. b (x e. t /\ t C_ o) -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o)))
45	30, 44	syl9r 72	. . . . . . . . . . . 12 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> (A.y e. o E.t e. b (y e. t /\ t C_ o) -> (x e. o -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o))))
46	45	adantld 426	. . . . . . . . . . 11 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> ((o C_ U.b /\ A.y e. o E.t e. b (y e. t /\ t C_ o)) -> (x e. o -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o))))
47	26, 46	sylbid 220	. . . . . . . . . 10 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> (o e. (topGen` b) -> (x e. o -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o))))
48	47	r19.21aiv 2175	. . . . . . . . 9 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> A.o e. (topGen` b)(x e. o -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o)))
49		breq1 3341	. . . . . . . . . . 11 |- (s = {q e. b | x e. q} -> (s ~<_ om <-> {q e. b | x e. q} ~<_ om))
50		rexeq 2267	. . . . . . . . . . . . 13 |- (s = {q e. b | x e. q} -> (E.p e. s (x e. p /\ p C_ o) <-> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o)))
51	50	imbi2d 674	. . . . . . . . . . . 12 |- (s = {q e. b | x e. q} -> ((x e. o -> E.p e. s (x e. p /\ p C_ o)) <-> (x e. o -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o))))
52	51	ralbidv 2123	. . . . . . . . . . 11 |- (s = {q e. b | x e. q} -> (A.o e. (topGen` b)(x e. o -> E.p e. s (x e. p /\ p C_ o)) <-> A.o e. (topGen` b)(x e. o -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o))))
53	49, 52	anbi12d 690	. . . . . . . . . 10 |- (s = {q e. b | x e. q} -> ((s ~<_ om /\ A.o e. (topGen` b)(x e. o -> E.p e. s (x e. p /\ p C_ o))) <-> ({q e. b | x e. q} ~<_ om /\ A.o e. (topGen` b)(x e. o -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o)))))
54	53	rcla4ev 2381	. . . . . . . . 9 |- (({q e. b | x e. q} e. ~P(topGen` b) /\ ({q e. b | x e. q} ~<_ om /\ A.o e. (topGen` b)(x e. o -> E.p e. {q e. b | x e. q} (x e. p /\ p C_ o)))) -> E.s e. ~P (topGen` b)(s ~<_ om /\ A.o e. (topGen` b)(x e. o -> E.p e. s (x e. p /\ p C_ o))))
55	16, 24, 48, 54	syl12anc 1098	. . . . . . . 8 |- ((b e. Bases /\ b ~<_ om /\ x e. U.(topGen` b)) -> E.s e. ~P (topGen` b)(s ~<_ om /\ A.o e. (topGen` b)(x e. o -> E.p e. s (x e. p /\ p C_ o))))
56	55	3expia 1069	. . . . . . 7 |- ((b e. Bases /\ b ~<_ om) -> (x e. U.(topGen` b) -> E.s e. ~P (topGen` b)(s ~<_ om /\ A.o e. (topGen` b)(x e. o -> E.p e. s (x e. p /\ p C_ o)))))
57	8, 56	syl5cbi 226	. . . . . 6 |- ((b e. Bases /\ b ~<_ om) -> ((topGen` b) = J -> (x e. U.J -> E.s e. ~P J(s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o))))))
58	57	expimpd 404	. . . . 5 |- (b e. Bases -> ((b ~<_ om /\ (topGen` b) = J) -> (x e. U.J -> E.s e. ~P J(s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o))))))
59	58	r19.23aiv 2211	. . . 4 |- (E.b e. Bases (b ~<_ om /\ (topGen` b) = J) -> (x e. U.J -> E.s e. ~P J(s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o)))))
60	1, 59	sylbi 216	. . 3 |- (J e. 2ndc -> (x e. U.J -> E.s e. ~P J(s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o)))))
61	60	r19.21aiv 2175	. 2 |- (J e. 2ndc -> A.x e. U.JE.s e. ~P J(s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o))))
62		2ndctop 15474	. . 3 |- (J e. 2ndc -> J e. Top)
63		eqid 1884	. . . 4 |- U.J = U.J
64	63	is1stc3 15469	. . 3 |- (J e. Top -> (J e. 1stc <-> A.x e. U.JE.s e. ~P J(s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o)))))
65	62, 64	syl 12	. 2 |- (J e. 2ndc -> (J e. 1stc <-> A.x e. U.JE.s e. ~P J(s ~<_ om /\ A.o e. J (x e. o -> E.p e. s (x e. p /\ p C_ o)))))
66	61, 65	mpbird 213	1 |- (J e. 2ndc -> J e. 1stc)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  ~Pcpw 3032  U.cuni 3177   class class class wbr 3338  omcom 3949  ` cfv 3998   ~<_ cdom 5424  Topctop 8857  Basesctb 8859  topGenctg 8860  1stcc1stc 15455  2ndcc2ndc 15456

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-en 5427  df-dom 5428  df-top 8861  df-bases 8863  df-topgen 8864  df-1stc 15461  df-2ndc 15462

Copyright terms: Public domain