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 ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐾 ∈ 𝐴 )