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	⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Top )
	haushmphlem.2	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑓 : ∪ 𝐾 –1-1→ ∪ 𝐽 ∧ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) ) → 𝐾 ∈ 𝐴 )
Assertion	haushmphlem	⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		haushmphlem.1	⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Top )
2		haushmphlem.2	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑓 : ∪ 𝐾 –1-1→ ∪ 𝐽 ∧ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) ) → 𝐾 ∈ 𝐴 )
3		hmphsym	⊢ ( 𝐽 ≃ 𝐾 → 𝐾 ≃ 𝐽 )
4		hmph	⊢ ( 𝐾 ≃ 𝐽 ↔ ( 𝐾 Homeo 𝐽 ) ≠ ∅ )
5		n0	⊢ ( ( 𝐾 Homeo 𝐽 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) )
6		simpl	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) ) → 𝐽 ∈ 𝐴 )
7		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
8		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
9	7 8	hmeof1o	⊢ ( 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) → 𝑓 : ∪ 𝐾 –1-1-onto→ ∪ 𝐽 )
10	9	adantl	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) ) → 𝑓 : ∪ 𝐾 –1-1-onto→ ∪ 𝐽 )
11		f1of1	⊢ ( 𝑓 : ∪ 𝐾 –1-1-onto→ ∪ 𝐽 → 𝑓 : ∪ 𝐾 –1-1→ ∪ 𝐽 )
12	10 11	syl	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) ) → 𝑓 : ∪ 𝐾 –1-1→ ∪ 𝐽 )
13		hmeocn	⊢ ( 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) → 𝑓 ∈ ( 𝐾 Cn 𝐽 ) )
14	13	adantl	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) ) → 𝑓 ∈ ( 𝐾 Cn 𝐽 ) )
15	6 12 14 2	syl3anc	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) ) → 𝐾 ∈ 𝐴 )
16	15	expcom	⊢ ( 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) → ( 𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴 ) )
17	16	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) → ( 𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴 ) )
18	5 17	sylbi	⊢ ( ( 𝐾 Homeo 𝐽 ) ≠ ∅ → ( 𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴 ) )
19	4 18	sylbi	⊢ ( 𝐾 ≃ 𝐽 → ( 𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴 ) )
20	3 19	syl	⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴 ) )