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 21066

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 21062	. 2 $/\$
3	1	alexsubALTlem4 21065	. . . . 5
4		selpw 3958	. . . . . . . . 9
5		eleq2 2518	. . . . . . . . . . . . . . . . . . 19
6	5	3ad2ant3 1031	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
7		eluni 4201	. . . . . . . . . . . . . . . . . . . 20 $/\$
8		ssel 3426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
9		eleq2 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10		tg2 19980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
11	10	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
12	9, 11	syl6bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
13	8, 12	sylan9r 664	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
14	13	3impia 1205	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
15		sseq2 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
16	15	rspcev 3150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
17	16	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
18	17	3ad2ant3 1031	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
19	18	anim2d 569	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
20	19	reximdv 2861	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
21	14, 20	syld 45	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
22	21	3expia 1210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
23	22	com23 81	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
24	23	impd 433	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
25	24	exlimdv 1779	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	7, 25	syl5bi 221	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
27	26	3adant3 1028	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
28	6, 27	sylbid 219	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
29		ssel 3426	. . . . . . . . . . . . . . . . . . . . . 22
30		elunii 4203	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
31	30	expcom 437	. . . . . . . . . . . . . . . . . . . . . . 23
32	6	biimprd 227	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
33	31, 32	sylan9r 664	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
34	29, 33	syl9r 74	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
35	34	rexlimdva 2879	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
36	35	com23 81	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
37	36	impd 433	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
38	37	rexlimdvw 2882	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
39	28, 38	impbid 194	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
40		elunirab 4210	. . . . . . . . . . . . . . . 16 $/\$
41	39, 40	syl6bbr 267	. . . . . . . . . . . . . . 15 $/\$ $/\$
42	41	eqrdv 2449	. . . . . . . . . . . . . 14 $/\$ $/\$
43		ssrab2 3514	. . . . . . . . . . . . . . . 16
44		fvex 5875	. . . . . . . . . . . . . . . . 17
45	44	elpw2 4567	. . . . . . . . . . . . . . . 16
46	43, 45	mpbir 213	. . . . . . . . . . . . . . 15
47		unieq 4206	. . . . . . . . . . . . . . . . . 18
48	47	eqeq2d 2461	. . . . . . . . . . . . . . . . 17
49		pweq 3954	. . . . . . . . . . . . . . . . . . 19
50	49	ineq1d 3633	. . . . . . . . . . . . . . . . . 18
51	50	rexeqdv 2994	. . . . . . . . . . . . . . . . 17
52	48, 51	imbi12d 322	. . . . . . . . . . . . . . . 16
53	52	rspcv 3146	. . . . . . . . . . . . . . 15
54	46, 53	ax-mp 5	. . . . . . . . . . . . . 14
55	42, 54	syl5com 31	. . . . . . . . . . . . 13 $/\$ $/\$
56		elfpw 7876	. . . . . . . . . . . . . . 15 $/\$
57		ssel 3426	. . . . . . . . . . . . . . . . . . . . . . 23
58		sseq1 3453	. . . . . . . . . . . . . . . . . . . . . . . . . 26
59	58	rexbidv 2901	. . . . . . . . . . . . . . . . . . . . . . . . 25
60	59	elrab 3196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
61	60	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . 23
62	57, 61	syl6 34	. . . . . . . . . . . . . . . . . . . . . 22
63	62	ralrimiv 2800	. . . . . . . . . . . . . . . . . . . . 21
64		sseq2 3454	. . . . . . . . . . . . . . . . . . . . . . 23
65	64	ac6sfi 7815	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
66	65	ex 436	. . . . . . . . . . . . . . . . . . . . 21 $/\$
67	63, 66	syl5 33	. . . . . . . . . . . . . . . . . . . 20 $/\$
68	67	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
69		simprll 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		frn 5735	. . . . . . . . . . . . . . . . . . . . . . . . 25
71	69, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		simplr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		ffn 5728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
74		dffn4 5799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
75	73, 74	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76	75	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
77	76	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78		fodomfi 7850	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
79	72, 77, 78	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80		domfi 7793	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
81	72, 79, 80	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	71, 81	jca 535	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83		elin 3617	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . 26
85	84	elpw2 4567	. . . . . . . . . . . . . . . . . . . . . . . . 25
86	85	anbi1i 701	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
87	83, 86	bitr2i 254	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
88	82, 87	sylib 200	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simprr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		uniiun 4331	. . . . . . . . . . . . . . . . . . . . . . . . . 26
91		simprlr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92		ss2iun 4294	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	90, 93	syl5eqss 3476	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		fniunfv 6152	. . . . . . . . . . . . . . . . . . . . . . . . . 26
96	69, 73, 95	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	94, 96	sseqtrd 3468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	89, 97	eqsstrd 3466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simpll2 1048	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	71, 99	sstrd 3442	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101		uniss 4219	. . . . . . . . . . . . . . . . . . . . . . . . 25
102	101, 1	syl6sseqr 3479	. . . . . . . . . . . . . . . . . . . . . . . 24
103	100, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	98, 103	eqssd 3449	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105		unieq 4206	. . . . . . . . . . . . . . . . . . . . . . . 24
106	105	eqeq2d 2461	. . . . . . . . . . . . . . . . . . . . . . 23
107	106	rspcev 3150	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
108	88, 104, 107	syl2anc 667	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	108	exp32 610	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
110	109	exlimdv 1779	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
111	68, 110	syld 45	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
112	111	ex 436	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	112	com23 81	. . . . . . . . . . . . . . . 16 $/\$ $/\$
114	113	impd 433	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
115	56, 114	syl5bi 221	. . . . . . . . . . . . . 14 $/\$ $/\$
116	115	rexlimdv 2877	. . . . . . . . . . . . 13 $/\$ $/\$
117	55, 116	syld 45	. . . . . . . . . . . 12 $/\$ $/\$
118	117	3exp 1207	. . . . . . . . . . 11
119	118	com34 86	. . . . . . . . . 10
120	119	com23 81	. . . . . . . . 9
121	4, 120	syl7bi 234	. . . . . . . 8
122	121	ralrimdv 2804	. . . . . . 7
123		fibas 19993	. . . . . . . . 9
124		tgcl 19985	. . . . . . . . 9
125	123, 124	ax-mp 5	. . . . . . . 8
126		eleq1 2517	. . . . . . . 8
127	125, 126	mpbiri 237	. . . . . . 7
128	122, 127	jctild 546	. . . . . 6 $/\$
129	1	iscmp 20403	. . . . . 6 $/\$
130	128, 129	syl6ibr 231	. . . . 5
131	3, 130	syld 45	. . . 4
132	131	imp 431	. . 3 $/\$
133	132	exlimiv 1776	. 2 $/\$
134	2, 133	impbii 191	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wex 1663

wcel 1887

wral 2737

wrex 2738

crab 2741

cin 3403

wss 3404

cpw 3951

cuni 4198

ciun 4278 class class class wbr 4402

crn 4835

wfn 5577

wf 5578

wfo 5580

cfv 5582

cdom 7567

cfn 7569

cfi 7924

ctg 15336

ctop 19917

ctb 19920

ccmp 20401

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-ac2 8893

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-rpss 6571 df-om 6693 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-en 7570 df-dom 7571 df-fin 7573 df-fi 7925 df-card 8373 df-ac 8547 df-topgen 15342 df-top 19921 df-bases 19922 df-cmp 20402

This theorem is referenced by: (None)

W3C validator