Metamath Proof Explorer


Theorem sshauslem

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 X=J
sshauslem.2 JAJTop
sshauslem.3 JAIX:X1-1XIXKCnJKA
Assertion sshauslem JAKTopOnXJKKA

Proof

Step Hyp Ref Expression
1 t1sep.1 X=J
2 sshauslem.2 JAJTop
3 sshauslem.3 JAIX:X1-1XIXKCnJKA
4 simp1 JAKTopOnXJKJA
5 f1oi IX:X1-1 ontoX
6 f1of1 IX:X1-1 ontoXIX:X1-1X
7 5 6 mp1i JAKTopOnXJKIX:X1-1X
8 simp3 JAKTopOnXJKJK
9 simp2 JAKTopOnXJKKTopOnX
10 2 3ad2ant1 JAKTopOnXJKJTop
11 1 toptopon JTopJTopOnX
12 10 11 sylib JAKTopOnXJKJTopOnX
13 ssidcn KTopOnXJTopOnXIXKCnJJK
14 9 12 13 syl2anc JAKTopOnXJKIXKCnJJK
15 8 14 mpbird JAKTopOnXJKIXKCnJ
16 4 7 15 3 syl3anc JAKTopOnXJKKA