Metamath Proof Explorer

Theorem sshauslem

Description: Lemma for sshaus and similar theorems. If the topological property A is preserved under injective preimages, then a topology finer than one with property A also has property A . (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypotheses t1sep.1 ⊢ X = ⋃ J
sshauslem.2 ⊢ J ∈ A → J ∈ Top
sshauslem.3 ⊢ J ∈ A ∧ I ↾ X : X ⟶ 1-1 X ∧ I ↾ X ∈ K Cn J → K ∈ A
Assertion sshauslem ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → K ∈ A

Proof

Step Hyp Ref Expression
1 t1sep.1 ⊢ X = ⋃ J
2 sshauslem.2 ⊢ J ∈ A → J ∈ Top
3 sshauslem.3 ⊢ J ∈ A ∧ I ↾ X : X ⟶ 1-1 X ∧ I ↾ X ∈ K Cn J → K ∈ A
4 simp1 ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → J ∈ A
5 f1oi ⊢ I ↾ X : X ⟶ 1-1 onto X
6 f1of1 ⊢ I ↾ X : X ⟶ 1-1 onto X → I ↾ X : X ⟶ 1-1 X
7 5 6 mp1i ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → I ↾ X : X ⟶ 1-1 X
8 simp3 ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → J ⊆ K
9 simp2 ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → K ∈ TopOn ⁡ X
10 2 3ad2ant1 ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → J ∈ Top
11 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
12 10 11 sylib ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → J ∈ TopOn ⁡ X
13 ssidcn ⊢ K ∈ TopOn ⁡ X ∧ J ∈ TopOn ⁡ X → I ↾ X ∈ K Cn J ↔ J ⊆ K
14 9 12 13 syl2anc ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → I ↾ X ∈ K Cn J ↔ J ⊆ K
15 8 14 mpbird ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → I ↾ X ∈ K Cn J
16 4 7 15 3 syl3anc ⊢ J ∈ A ∧ K ∈ TopOn ⁡ X ∧ J ⊆ K → K ∈ A