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 ⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ 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 ⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴 ) )