Description: Lemma for alexsubALT . A compact space has a subbase such that every cover taken from it has a finite subcover. (Contributed by Jeff Hankins, 27-Jan-2010)
Ref | Expression | ||
---|---|---|---|
Hypothesis | alexsubALT.1 | |
|
Assertion | alexsubALTlem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alexsubALT.1 | |
|
2 | cmptop | |
|
3 | fitop | |
|
4 | 3 | fveq2d | |
5 | tgtop | |
|
6 | 4 5 | eqtr2d | |
7 | 2 6 | syl | |
8 | velpw | |
|
9 | 1 | cmpcov | |
10 | 9 | 3exp | |
11 | 8 10 | syl5bi | |
12 | 11 | ralrimiv | |
13 | 2fveq3 | |
|
14 | 13 | eqeq2d | |
15 | pweq | |
|
16 | 15 | raleqdv | |
17 | 14 16 | anbi12d | |
18 | 17 | spcegv | |
19 | 7 12 18 | mp2and | |