Theorem dis2ndc 20255

Description: A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.)

Assertion

Ref	Expression
dis2ndc	|- ( X ~<_ om <-> ~P X e. 2ndc )

Proof of Theorem dis2ndc

Dummy variables w b x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reldom 7562	. . 3 |- Rel ~<_
2	1	brrelexi 4866	. 2 |- ( X ~<_ om -> X e. _V )
3		elex 3070	. . 3 |- ( ~P X e. 2ndc -> ~P X e. _V )
4		pwexb 6595	. . 3 |- ( X e. _V <-> ~P X e. _V )
5	3, 4	sylibr 214	. 2 |- ( ~P X e. 2ndc -> X e. _V )
6		elex 3070	. . . . 5 |- ( X e. _V -> X e. _V )
7		snex 4634	. . . . . . . 8 |- { x } e. _V
8	7	2a1i 12	. . . . . . 7 |- ( X e. _V -> ( x e. X -> { x } e. _V ) )
9		vex 3064	. . . . . . . . . 10 |- x e. _V
10	9	sneqr 4141	. . . . . . . . 9 |- ( { x } = { y } -> x = y )
11		sneq 3984	. . . . . . . . 9 |- ( x = y -> { x } = { y } )
12	10, 11	impbii 189	. . . . . . . 8 |- ( { x } = { y } <-> x = y )
13	12	2a1i 12	. . . . . . 7 |- ( X e. _V -> ( ( x e. X /\ y e. X ) -> ( { x } = { y } <-> x = y ) ) )
14	8, 13	dom2lem 7595	. . . . . 6 |- ( X e. _V -> ( x e. X |-> { x } ) : X -1-1-> _V )
15		f1f1orn 5812	. . . . . 6 |- ( ( x e. X |-> { x } ) : X -1-1-> _V -> ( x e. X |-> { x } ) : X -1-1-onto-> ran ( x e. X |-> { x } ) )
16	14, 15	syl 17	. . . . 5 |- ( X e. _V -> ( x e. X |-> { x } ) : X -1-1-onto-> ran ( x e. X |-> { x } ) )
17		f1oeng 7574	. . . . 5 |- ( ( X e. _V /\ ( x e. X |-> { x } ) : X -1-1-onto-> ran ( x e. X |-> { x } ) ) -> X ~~ ran ( x e. X |-> { x } ) )
18	6, 16, 17	syl2anc 661	. . . 4 |- ( X e. _V -> X ~~ ran ( x e. X |-> { x } ) )
19		domen1 7699	. . . 4 |- ( X ~~ ran ( x e. X |-> { x } ) -> ( X ~<_ om <-> ran ( x e. X |-> { x } ) ~<_ om ) )
20	18, 19	syl 17	. . 3 |- ( X e. _V -> ( X ~<_ om <-> ran ( x e. X |-> { x } ) ~<_ om ) )
21		distop 19791	. . . . . . 7 |- ( X e. _V -> ~P X e. Top )
22		simpr 461	. . . . . . . . . 10 |- ( ( X e. _V /\ x e. X ) -> x e. X )
23	9	snelpw 4639	. . . . . . . . . 10 |- ( x e. X <-> { x } e. ~P X )
24	22, 23	sylib 198	. . . . . . . . 9 |- ( ( X e. _V /\ x e. X ) -> { x } e. ~P X )
25		eqid 2404	. . . . . . . . 9 |- ( x e. X |-> { x } ) = ( x e. X |-> { x } )
26	24, 25	fmptd 6035	. . . . . . . 8 |- ( X e. _V -> ( x e. X |-> { x } ) : X --> ~P X )
27		frn 5722	. . . . . . . 8 |- ( ( x e. X |-> { x } ) : X --> ~P X -> ran ( x e. X |-> { x } ) C_ ~P X )
28	26, 27	syl 17	. . . . . . 7 |- ( X e. _V -> ran ( x e. X |-> { x } ) C_ ~P X )
29		elpwi 3966	. . . . . . . . . . . . 13 |- ( y e. ~P X -> y C_ X )
30	29	ad2antrl 728	. . . . . . . . . . . 12 |- ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> y C_ X )
31		simprr 760	. . . . . . . . . . . 12 |- ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> z e. y )
32	30, 31	sseldd 3445	. . . . . . . . . . 11 |- ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> z e. X )
33		eqidd 2405	. . . . . . . . . . 11 |- ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> { z } = { z } )
34		sneq 3984	. . . . . . . . . . . . 13 |- ( x = z -> { x } = { z } )
35	34	eqeq2d 2418	. . . . . . . . . . . 12 |- ( x = z -> ( { z } = { x } <-> { z } = { z } ) )
36	35	rspcev 3162	. . . . . . . . . . 11 |- ( ( z e. X /\ { z } = { z } ) -> E. x e. X { z } = { x } )
37	32, 33, 36	syl2anc 661	. . . . . . . . . 10 |- ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> E. x e. X { z } = { x } )
38		snex 4634	. . . . . . . . . . 11 |- { z } e. _V
39	25	elrnmpt 5072	. . . . . . . . . . 11 |- ( { z } e. _V -> ( { z } e. ran ( x e. X |-> { x } ) <-> E. x e. X { z } = { x } ) )
40	38, 39	ax-mp 5	. . . . . . . . . 10 |- ( { z } e. ran ( x e. X |-> { x } ) <-> E. x e. X { z } = { x } )
41	37, 40	sylibr 214	. . . . . . . . 9 |- ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> { z } e. ran ( x e. X |-> { x } ) )
42		ssnid 4003	. . . . . . . . . 10 |- z e. { z }
43	42	a1i 11	. . . . . . . . 9 |- ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> z e. { z } )
44	31	snssd 4119	. . . . . . . . 9 |- ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> { z } C_ y )
45		eleq2 2477	. . . . . . . . . . 11 |- ( w = { z } -> ( z e. w <-> z e. { z } ) )
46		sseq1 3465	. . . . . . . . . . 11 |- ( w = { z } -> ( w C_ y <-> { z } C_ y ) )
47	45, 46	anbi12d 711	. . . . . . . . . 10 |- ( w = { z } -> ( ( z e. w /\ w C_ y ) <-> ( z e. { z } /\ { z } C_ y ) ) )
48	47	rspcev 3162	. . . . . . . . 9 |- ( ( { z } e. ran ( x e. X |-> { x } ) /\ ( z e. { z } /\ { z } C_ y ) ) -> E. w e. ran ( x e. X |-> { x } ) ( z e. w /\ w C_ y ) )
49	41, 43, 44, 48	syl12anc 1230	. . . . . . . 8 |- ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> E. w e. ran ( x e. X |-> { x } ) ( z e. w /\ w C_ y ) )
50	49	ralrimivva 2827	. . . . . . 7 |- ( X e. _V -> A. y e. ~P X A. z e. y E. w e. ran ( x e. X |-> { x } ) ( z e. w /\ w C_ y ) )
51		basgen2 19785	. . . . . . 7 |- ( ( ~P X e. Top /\ ran ( x e. X |-> { x } ) C_ ~P X /\ A. y e. ~P X A. z e. y E. w e. ran ( x e. X |-> { x } ) ( z e. w /\ w C_ y ) ) -> ( topGen ` ran ( x e. X |-> { x } ) ) = ~P X )
52	21, 28, 50, 51	syl3anc 1232	. . . . . 6 |- ( X e. _V -> ( topGen ` ran ( x e. X |-> { x } ) ) = ~P X )
53	52	adantr 465	. . . . 5 |- ( ( X e. _V /\ ran ( x e. X |-> { x } ) ~<_ om ) -> ( topGen ` ran ( x e. X |-> { x } ) ) = ~P X )
54	52, 21	eqeltrd 2492	. . . . . . 7 |- ( X e. _V -> ( topGen ` ran ( x e. X |-> { x } ) ) e. Top )
55		tgclb 19766	. . . . . . 7 |- ( ran ( x e. X |-> { x } ) e. TopBases <-> ( topGen ` ran ( x e. X |-> { x } ) ) e. Top )
56	54, 55	sylibr 214	. . . . . 6 |- ( X e. _V -> ran ( x e. X |-> { x } ) e. TopBases )
57		2ndci 20243	. . . . . 6 |- ( ( ran ( x e. X |-> { x } ) e. TopBases /\ ran ( x e. X |-> { x } ) ~<_ om ) -> ( topGen ` ran ( x e. X |-> { x } ) ) e. 2ndc )
58	56, 57	sylan 471	. . . . 5 |- ( ( X e. _V /\ ran ( x e. X |-> { x } ) ~<_ om ) -> ( topGen ` ran ( x e. X |-> { x } ) ) e. 2ndc )
59	53, 58	eqeltrrd 2493	. . . 4 |- ( ( X e. _V /\ ran ( x e. X |-> { x } ) ~<_ om ) -> ~P X e. 2ndc )
60		is2ndc 20241	. . . . . 6 |- ( ~P X e. 2ndc <-> E. b e. TopBases ( b ~<_ om /\ ( topGen ` b ) = ~P X ) )
61		vex 3064	. . . . . . . . . 10 |- b e. _V
62		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> x e. X )
63	62, 23	sylib 198	. . . . . . . . . . . . . . 15 |- ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> { x } e. ~P X )
64		simplrr 765	. . . . . . . . . . . . . . 15 |- ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> ( topGen ` b ) = ~P X )
65	63, 64	eleqtrrd 2495	. . . . . . . . . . . . . 14 |- ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> { x } e. ( topGen ` b ) )
66		ssnid 4003	. . . . . . . . . . . . . 14 |- x e. { x }
67		tg2 19760	. . . . . . . . . . . . . 14 |- ( ( { x } e. ( topGen ` b ) /\ x e. { x } ) -> E. y e. b ( x e. y /\ y C_ { x } ) )
68	65, 66, 67	sylancl 662	. . . . . . . . . . . . 13 |- ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> E. y e. b ( x e. y /\ y C_ { x } ) )
69		simprrl 768	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> x e. y )
70	69	snssd 4119	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> { x } C_ y )
71		simprrr 769	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> y C_ { x } )
72	70, 71	eqssd 3461	. . . . . . . . . . . . . 14 |- ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> { x } = y )
73		simprl 758	. . . . . . . . . . . . . 14 |- ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> y e. b )
74	72, 73	eqeltrd 2492	. . . . . . . . . . . . 13 |- ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> { x } e. b )
75	68, 74	rexlimddv 2902	. . . . . . . . . . . 12 |- ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> { x } e. b )
76	75, 25	fmptd 6035	. . . . . . . . . . 11 |- ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) -> ( x e. X |-> { x } ) : X --> b )
77		frn 5722	. . . . . . . . . . 11 |- ( ( x e. X |-> { x } ) : X --> b -> ran ( x e. X |-> { x } ) C_ b )
78	76, 77	syl 17	. . . . . . . . . 10 |- ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) -> ran ( x e. X |-> { x } ) C_ b )
79		ssdomg 7601	. . . . . . . . . 10 |- ( b e. _V -> ( ran ( x e. X |-> { x } ) C_ b -> ran ( x e. X |-> { x } ) ~<_ b ) )
80	61, 78, 79	mpsyl 64	. . . . . . . . 9 |- ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) -> ran ( x e. X |-> { x } ) ~<_ b )
81		simprl 758	. . . . . . . . 9 |- ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) -> b ~<_ om )
82		domtr 7608	. . . . . . . . 9 |- ( ( ran ( x e. X |-> { x } ) ~<_ b /\ b ~<_ om ) -> ran ( x e. X |-> { x } ) ~<_ om )
83	80, 81, 82	syl2anc 661	. . . . . . . 8 |- ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ om /\ ( topGen ` b ) = ~P X ) ) -> ran ( x e. X |-> { x } ) ~<_ om )
84	83	ex 434	. . . . . . 7 |- ( ( X e. _V /\ b e. TopBases ) -> ( ( b ~<_ om /\ ( topGen ` b ) = ~P X ) -> ran ( x e. X |-> { x } ) ~<_ om ) )
85	84	rexlimdva 2898	. . . . . 6 |- ( X e. _V -> ( E. b e. TopBases ( b ~<_ om /\ ( topGen ` b ) = ~P X ) -> ran ( x e. X |-> { x } ) ~<_ om ) )
86	60, 85	syl5bi 219	. . . . 5 |- ( X e. _V -> ( ~P X e. 2ndc -> ran ( x e. X |-> { x } ) ~<_ om ) )
87	86	imp 429	. . . 4 |- ( ( X e. _V /\ ~P X e. 2ndc ) -> ran ( x e. X |-> { x } ) ~<_ om )
88	59, 87	impbida 835	. . 3 |- ( X e. _V -> ( ran ( x e. X |-> { x } ) ~<_ om <-> ~P X e. 2ndc ) )
89	20, 88	bitrd 255	. 2 |- ( X e. _V -> ( X ~<_ om <-> ~P X e. 2ndc ) )
90	2, 5, 89	pm5.21nii 353	1 |- ( X ~<_ om <-> ~P X e. 2ndc )

Syntax hints:   <-> wb 186   /\ wa 369   = wceq 1407   e. wcel 1844   A.wral 2756   E.wrex 2757   _Vcvv 3061   C_ wss 3416   ~Pcpw 3957   {csn 3974   class class class wbr 4397   |-> cmpt 4455   ran crn 4826   -->wf 5567   -1-1->wf1 5568   -1-1-onto->wf1o 5570   ` cfv 5571   omcom 6685   ~~ cen 7553   ~<_ cdom 7554   topGenctg 15054   Topctop 19688   TopBasesctb 19692   2ndcc2ndc 20233

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-iun 4275  df-br 4398  df-opab 4456  df-mpt 4457  df-id 4740  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-er 7350  df-en 7557  df-dom 7558  df-topgen 15060  df-top 19693  df-bases 19695  df-2ndc 20235

This theorem is referenced by: (None)