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 \in A \to J \in Top$
	haushmphlem.2	$⊢ (J \in A \land f : ⋃ K \underset{1-1}{⟶} ⋃ J \land f \in (K Cn J)) \to K \in A$
Assertion	haushmphlem	$⊢ J ≃ K \to (J \in A \to K \in A)$

Proof

Step	Hyp	Ref	Expression
1		haushmphlem.1	$⊢ J \in A \to J \in Top$
2		haushmphlem.2	$⊢ (J \in A \land f : ⋃ K \underset{1-1}{⟶} ⋃ J \land f \in (K Cn J)) \to K \in A$
3		hmphsym	$⊢ J ≃ K \to K ≃ J$
4		hmph	$⊢ K ≃ J \leftrightarrow K Homeo J \neq \emptyset$
5		n0	$⊢ K Homeo J \neq \emptyset \leftrightarrow \exists f f \in (K Homeo J)$
6		simpl	$⊢ (J \in A \land f \in (K Homeo J)) \to J \in A$
7		eqid	$⊢ ⋃ K = ⋃ K$
8		eqid	$⊢ ⋃ J = ⋃ J$
9	7 8	hmeof1o	$⊢ f \in (K Homeo J) \to f : ⋃ K \underset{1-1 onto}{⟶} ⋃ J$
10	9	adantl	$⊢ (J \in A \land f \in (K Homeo J)) \to f : ⋃ K \underset{1-1 onto}{⟶} ⋃ J$
11		f1of1	$⊢ f : ⋃ K \underset{1-1 onto}{⟶} ⋃ J \to f : ⋃ K \underset{1-1}{⟶} ⋃ J$
12	10 11	syl	$⊢ (J \in A \land f \in (K Homeo J)) \to f : ⋃ K \underset{1-1}{⟶} ⋃ J$
13		hmeocn	$⊢ f \in (K Homeo J) \to f \in (K Cn J)$
14	13	adantl	$⊢ (J \in A \land f \in (K Homeo J)) \to f \in (K Cn J)$
15	6 12 14 2	syl3anc	$⊢ (J \in A \land f \in (K Homeo J)) \to K \in A$
16	15	expcom	$⊢ f \in (K Homeo J) \to (J \in A \to K \in A)$
17	16	exlimiv	$⊢ \exists f f \in (K Homeo J) \to (J \in A \to K \in A)$
18	5 17	sylbi	$⊢ K Homeo J \neq \emptyset \to (J \in A \to K \in A)$
19	4 18	sylbi	$⊢ K ≃ J \to (J \in A \to K \in A)$
20	3 19	syl	$⊢ J ≃ K \to (J \in A \to K \in A)$

Metamath Proof Explorer

Theorem haushmphlem

Proof