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

Metamath Proof Explorer

Theorem haushmphlem

Description: Lemma for haushmph and similar theorems. If the topological property A is preserved under injective preimages, then property A is preserved under homeomorphisms. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypotheses haushmphlem.1 
|- ( J e. A -> J e. Top )
haushmphlem.2 
|- ( ( J e. A /\ f : U. K -1-1-> U. J /\ f e. ( K Cn J ) ) -> K e. A )
Assertion haushmphlem 
|- ( J ~= K -> ( J e. A -> K e. A ) )

Proof

Step Hyp Ref Expression
1 haushmphlem.1 
 |-  ( J e. A -> J e. Top )
2 haushmphlem.2 
 |-  ( ( J e. A /\ f : U. K -1-1-> U. J /\ f e. ( K Cn J ) ) -> K e. A )
3 hmphsym 
 |-  ( J ~= K -> K ~= J )
4 hmph 
 |-  ( K ~= J <-> ( K Homeo J ) =/= (/) )
5 n0 
 |-  ( ( K Homeo J ) =/= (/) <-> E. f f e. ( K Homeo J ) )
6 simpl 
 |-  ( ( J e. A /\ f e. ( K Homeo J ) ) -> J e. A )
7 eqid 
 |-  U. K = U. K
8 eqid 
 |-  U. J = U. J
9 7 8 hmeof1o 
 |-  ( f e. ( K Homeo J ) -> f : U. K -1-1-onto-> U. J )
10 9 adantl 
 |-  ( ( J e. A /\ f e. ( K Homeo J ) ) -> f : U. K -1-1-onto-> U. J )
11 f1of1 
 |-  ( f : U. K -1-1-onto-> U. J -> f : U. K -1-1-> U. J )
12 10 11 syl 
 |-  ( ( J e. A /\ f e. ( K Homeo J ) ) -> f : U. K -1-1-> U. J )
13 hmeocn 
 |-  ( f e. ( K Homeo J ) -> f e. ( K Cn J ) )
14 13 adantl 
 |-  ( ( J e. A /\ f e. ( K Homeo J ) ) -> f e. ( K Cn J ) )
15 6 12 14 2 syl3anc 
 |-  ( ( J e. A /\ f e. ( K Homeo J ) ) -> K e. A )
16 15 expcom 
 |-  ( f e. ( K Homeo J ) -> ( J e. A -> K e. A ) )
17 16 exlimiv 
 |-  ( E. f f e. ( K Homeo J ) -> ( J e. A -> K e. A ) )
18 5 17 sylbi 
 |-  ( ( K Homeo J ) =/= (/) -> ( J e. A -> K e. A ) )
19 4 18 sylbi 
 |-  ( K ~= J -> ( J e. A -> K e. A ) )
20 3 19 syl 
 |-  ( J ~= K -> ( J e. A -> K e. A ) )