This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
sshauslem.2 ⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Top )
sshauslem.3 ⊢ ( ( 𝐽 ∈ 𝐴 ∧ ( I ↾ 𝑋 ) : 𝑋 –1-1→ 𝑋 ∧ ( I ↾ 𝑋 ) ∈ ( 𝐾 Cn 𝐽 ) ) → 𝐾 ∈ 𝐴 )
Assertion sshauslem ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐾 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 t1sep.1 ⊢ 𝑋 = ∪ 𝐽
2 sshauslem.2 ⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Top )
3 sshauslem.3 ⊢ ( ( 𝐽 ∈ 𝐴 ∧ ( I ↾ 𝑋 ) : 𝑋 –1-1→ 𝑋 ∧ ( I ↾ 𝑋 ) ∈ ( 𝐾 Cn 𝐽 ) ) → 𝐾 ∈ 𝐴 )
4 simp1 ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐽 ∈ 𝐴 )
5 f1oi ⊢ ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋
6 f1of1 ⊢ ( ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋 → ( I ↾ 𝑋 ) : 𝑋 –1-1→ 𝑋 )
7 5 6 mp1i ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( I ↾ 𝑋 ) : 𝑋 –1-1→ 𝑋 )
8 simp3 ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐽 ⊆ 𝐾 )
9 simp2 ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
10 2 3ad2ant1 ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐽 ∈ Top )
11 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
12 10 11 sylib ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
13 ssidcn ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐾 Cn 𝐽 ) ↔ 𝐽 ⊆ 𝐾 ) )
14 9 12 13 syl2anc ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐾 Cn 𝐽 ) ↔ 𝐽 ⊆ 𝐾 ) )
15 8 14 mpbird ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( I ↾ 𝑋 ) ∈ ( 𝐾 Cn 𝐽 ) )
16 4 7 15 3 syl3anc ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐾 ∈ 𝐴 )