Metamath Proof Explorer

Theorem qtopss

Description: A surjective continuous function from J to K induces a topology J qTop F on the base set of K . This topology is in general finer than K . Together with qtopid , this implies that J qTop F is the finest topology making F continuous, i.e. the final topology with respect to the family { F } . (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Assertion qtopss ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) → 𝐾 ⊆ ( 𝐽 qTop 𝐹 ) )

Proof

Step Hyp Ref Expression
1 toponss ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ⊆ 𝑌 )
2 1 3ad2antl2 ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ⊆ 𝑌 )
3 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
4 3 3ad2antl1 ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
5 simpl1 ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
6 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
7 5 6 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐽 ∈ Top )
8 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
9 7 8 sylib ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
10 simpl2 ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
11 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
12 9 10 5 11 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
13 12 ffnd ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐹 Fn ∪ 𝐽 )
14 simpl3 ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ran 𝐹 = 𝑌 )
15 df-fo ⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 ↔ ( 𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 = 𝑌 ) )
16 13 14 15 sylanbrc ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐹 : ∪ 𝐽 –onto→ 𝑌 )
17 elqtop3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 : ∪ 𝐽 –onto→ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
18 9 16 17 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
19 2 4 18 mpbir2and ⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ∈ ( 𝐽 qTop 𝐹 ) )
20 19 ex ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) → ( 𝑥 ∈ 𝐾 → 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ) )
21 20 ssrdv ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) → 𝐾 ⊆ ( 𝐽 qTop 𝐹 ) )