Description: Lemma for sshaus and similar theorems. If the topological property A is preserved under injective preimages, then a topology finer than one with property A also has property A . (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | t1sep.1 | |
|
sshauslem.2 | |
||
sshauslem.3 | |
||
Assertion | sshauslem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | t1sep.1 | |
|
2 | sshauslem.2 | |
|
3 | sshauslem.3 | |
|
4 | simp1 | |
|
5 | f1oi | |
|
6 | f1of1 | |
|
7 | 5 6 | mp1i | |
8 | simp3 | |
|
9 | simp2 | |
|
10 | 2 | 3ad2ant1 | |
11 | 1 | toptopon | |
12 | 10 11 | sylib | |
13 | ssidcn | |
|
14 | 9 12 13 | syl2anc | |
15 | 8 14 | mpbird | |
16 | 4 7 15 3 | syl3anc | |