This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = U. J
sshauslem.2 
|- ( J e. A -> J e. Top )
sshauslem.3 
|- ( ( J e. A /\ ( _I |` X ) : X -1-1-> X /\ ( _I |` X ) e. ( K Cn J ) ) -> K e. A )
Assertion sshauslem 
|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. A )

Proof

Step Hyp Ref Expression
1 t1sep.1 
 |-  X = U. J
2 sshauslem.2 
 |-  ( J e. A -> J e. Top )
3 sshauslem.3 
 |-  ( ( J e. A /\ ( _I |` X ) : X -1-1-> X /\ ( _I |` X ) e. ( K Cn J ) ) -> K e. A )
4 simp1 
 |-  ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> J e. A )
5 f1oi 
 |-  ( _I |` X ) : X -1-1-onto-> X
6 f1of1 
 |-  ( ( _I |` X ) : X -1-1-onto-> X -> ( _I |` X ) : X -1-1-> X )
7 5 6 mp1i 
 |-  ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( _I |` X ) : X -1-1-> X )
8 simp3 
 |-  ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> J C_ K )
9 simp2 
 |-  ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. ( TopOn ` X ) )
10 2 3ad2ant1 
 |-  ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> J e. Top )
11 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
12 10 11 sylib 
 |-  ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> J e. ( TopOn ` X ) )
13 ssidcn 
 |-  ( ( K e. ( TopOn ` X ) /\ J e. ( TopOn ` X ) ) -> ( ( _I |` X ) e. ( K Cn J ) <-> J C_ K ) )
14 9 12 13 syl2anc 
 |-  ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( ( _I |` X ) e. ( K Cn J ) <-> J C_ K ) )
15 8 14 mpbird 
 |-  ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( _I |` X ) e. ( K Cn J ) )
16 4 7 15 3 syl3anc 
 |-  ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. A )