alexsubALT - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > alexsubALT		Structured version Visualization version Unicode version

Theorem alexsubALT 21144

Description: The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 11-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.)

**Hypothesis**
Ref	Expression
alexsubALT.1

**Assertion**
Ref	Expression
alexsubALT	$/\$

Distinct variable groups:

Proof of Theorem alexsubALT Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		alexsubALT.1	. . 3
2	1	alexsubALTlem1 21140	. 2 $/\$
3	1	alexsubALTlem4 21143	. . . . 5
4		selpw 3949	. . . . . . . . 9
5		eleq2 2538	. . . . . . . . . . . . . . . . . . 19
6	5	3ad2ant3 1053	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
7		eluni 4193	. . . . . . . . . . . . . . . . . . . 20 $/\$
8		ssel 3412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
9		eleq2 2538	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10		tg2 20057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
11	10	ex 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
12	9, 11	syl6bi 236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
13	8, 12	sylan9r 670	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
14	13	3impia 1228	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
15		sseq2 3440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
16	15	rspcev 3136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
17	16	ex 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
18	17	3ad2ant3 1053	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
19	18	anim2d 575	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
20	19	reximdv 2857	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
21	14, 20	syld 44	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
22	21	3expia 1233	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
23	22	com23 80	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
24	23	impd 438	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
25	24	exlimdv 1787	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	7, 25	syl5bi 225	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
27	26	3adant3 1050	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
28	6, 27	sylbid 223	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
29		ssel 3412	. . . . . . . . . . . . . . . . . . . . . 22
30		elunii 4195	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
31	30	expcom 442	. . . . . . . . . . . . . . . . . . . . . . 23
32	6	biimprd 231	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
33	31, 32	sylan9r 670	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
34	29, 33	syl9r 73	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
35	34	rexlimdva 2871	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
36	35	com23 80	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
37	36	impd 438	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
38	37	rexlimdvw 2874	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
39	28, 38	impbid 195	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
40		elunirab 4202	. . . . . . . . . . . . . . . 16 $/\$
41	39, 40	syl6bbr 271	. . . . . . . . . . . . . . 15 $/\$ $/\$
42	41	eqrdv 2469	. . . . . . . . . . . . . 14 $/\$ $/\$
43		ssrab2 3500	. . . . . . . . . . . . . . . 16
44		fvex 5889	. . . . . . . . . . . . . . . . 17
45	44	elpw2 4565	. . . . . . . . . . . . . . . 16
46	43, 45	mpbir 214	. . . . . . . . . . . . . . 15
47		unieq 4198	. . . . . . . . . . . . . . . . . 18
48	47	eqeq2d 2481	. . . . . . . . . . . . . . . . 17
49		pweq 3945	. . . . . . . . . . . . . . . . . . 19
50	49	ineq1d 3624	. . . . . . . . . . . . . . . . . 18
51	50	rexeqdv 2980	. . . . . . . . . . . . . . . . 17
52	48, 51	imbi12d 327	. . . . . . . . . . . . . . . 16
53	52	rspcv 3132	. . . . . . . . . . . . . . 15
54	46, 53	ax-mp 5	. . . . . . . . . . . . . 14
55	42, 54	syl5com 30	. . . . . . . . . . . . 13 $/\$ $/\$
56		elfpw 7894	. . . . . . . . . . . . . . 15 $/\$
57		ssel 3412	. . . . . . . . . . . . . . . . . . . . . . 23
58		sseq1 3439	. . . . . . . . . . . . . . . . . . . . . . . . . 26
59	58	rexbidv 2892	. . . . . . . . . . . . . . . . . . . . . . . . 25
60	59	elrab 3184	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
61	60	simprbi 471	. . . . . . . . . . . . . . . . . . . . . . 23
62	57, 61	syl6 33	. . . . . . . . . . . . . . . . . . . . . 22
63	62	ralrimiv 2808	. . . . . . . . . . . . . . . . . . . . 21
64		sseq2 3440	. . . . . . . . . . . . . . . . . . . . . . 23
65	64	ac6sfi 7833	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
66	65	ex 441	. . . . . . . . . . . . . . . . . . . . 21 $/\$
67	63, 66	syl5 32	. . . . . . . . . . . . . . . . . . . 20 $/\$
68	67	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
69		simprll 780	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		frn 5747	. . . . . . . . . . . . . . . . . . . . . . . . 25
71	69, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		simplr 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		ffn 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
74		dffn4 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
75	73, 74	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76	75	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
77	76	ad2antrl 742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78		fodomfi 7868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
79	72, 77, 78	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80		domfi 7811	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
81	72, 79, 80	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	71, 81	jca 541	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83		elin 3608	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . 26
85	84	elpw2 4565	. . . . . . . . . . . . . . . . . . . . . . . . 25
86	85	anbi1i 709	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
87	83, 86	bitr2i 258	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
88	82, 87	sylib 201	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simprr 774	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		uniiun 4322	. . . . . . . . . . . . . . . . . . . . . . . . . 26
91		simprlr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92		ss2iun 4285	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	90, 93	syl5eqss 3462	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		fniunfv 6170	. . . . . . . . . . . . . . . . . . . . . . . . . 26
96	69, 73, 95	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	94, 96	sseqtrd 3454	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	89, 97	eqsstrd 3452	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simpll2 1070	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	71, 99	sstrd 3428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101		uniss 4211	. . . . . . . . . . . . . . . . . . . . . . . . 25
102	101, 1	syl6sseqr 3465	. . . . . . . . . . . . . . . . . . . . . . . 24
103	100, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	98, 103	eqssd 3435	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105		unieq 4198	. . . . . . . . . . . . . . . . . . . . . . . 24
106	105	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . 23
107	106	rspcev 3136	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
108	88, 104, 107	syl2anc 673	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	108	exp32 616	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
110	109	exlimdv 1787	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
111	68, 110	syld 44	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
112	111	ex 441	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	112	com23 80	. . . . . . . . . . . . . . . 16 $/\$ $/\$
114	113	impd 438	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
115	56, 114	syl5bi 225	. . . . . . . . . . . . . 14 $/\$ $/\$
116	115	rexlimdv 2870	. . . . . . . . . . . . 13 $/\$ $/\$
117	55, 116	syld 44	. . . . . . . . . . . 12 $/\$ $/\$
118	117	3exp 1230	. . . . . . . . . . 11
119	118	com34 85	. . . . . . . . . 10
120	119	com23 80	. . . . . . . . 9
121	4, 120	syl7bi 238	. . . . . . . 8
122	121	ralrimdv 2811	. . . . . . 7
123		fibas 20070	. . . . . . . . 9
124		tgcl 20062	. . . . . . . . 9
125	123, 124	ax-mp 5	. . . . . . . 8
126		eleq1 2537	. . . . . . . 8
127	125, 126	mpbiri 241	. . . . . . 7
128	122, 127	jctild 552	. . . . . 6 $/\$
129	1	iscmp 20480	. . . . . 6 $/\$
130	128, 129	syl6ibr 235	. . . . 5
131	3, 130	syld 44	. . . 4
132	131	imp 436	. . 3 $/\$
133	132	exlimiv 1784	. 2 $/\$
134	2, 133	impbii 192	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wex 1671

wcel 1904

wral 2756

wrex 2757

crab 2760

cin 3389

wss 3390

cpw 3942

cuni 4190

ciun 4269 class class class wbr 4395

crn 4840

wfn 5584

wf 5585

wfo 5587

cfv 5589

cdom 7585

cfn 7587

cfi 7942

ctg 15414

ctop 19994

ctb 19997

ccmp 20478

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-ac2 8911

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-rpss 6590 df-om 6712 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-en 7588 df-dom 7589 df-fin 7591 df-fi 7943 df-card 8391 df-ac 8565 df-topgen 15420 df-top 19998 df-bases 19999 df-cmp 20479

This theorem is referenced by: (None)

W3C validator