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 ) )