Metamath Proof Explorer

Theorem imastps

Description: The image of a topological space under a function is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses imastps.u ⊢ φ → U = F “ 𝑠 R
imastps.v ⊢ φ → V = Base R
imastps.f ⊢ φ → F : V ⟶ onto B
imastps.r ⊢ φ → R ∈ TopSp
Assertion imastps ⊢ φ → U ∈ TopSp

Proof

Step Hyp Ref Expression
1 imastps.u ⊢ φ → U = F “ 𝑠 R
2 imastps.v ⊢ φ → V = Base R
3 imastps.f ⊢ φ → F : V ⟶ onto B
4 imastps.r ⊢ φ → R ∈ TopSp
5 eqid ⊢ TopOpen ⁡ R = TopOpen ⁡ R
6 eqid ⊢ TopOpen ⁡ U = TopOpen ⁡ U
7 1 2 3 4 5 6 imastopn ⊢ φ → TopOpen ⁡ U = TopOpen ⁡ R qTop F
8 eqid ⊢ Base R = Base R
9 8 5 istps ⊢ R ∈ TopSp ↔ TopOpen ⁡ R ∈ TopOn ⁡ Base R
10 4 9 sylib ⊢ φ → TopOpen ⁡ R ∈ TopOn ⁡ Base R
11 2 fveq2d ⊢ φ → TopOn ⁡ V = TopOn ⁡ Base R
12 10 11 eleqtrrd ⊢ φ → TopOpen ⁡ R ∈ TopOn ⁡ V
13 qtoptopon ⊢ TopOpen ⁡ R ∈ TopOn ⁡ V ∧ F : V ⟶ onto B → TopOpen ⁡ R qTop F ∈ TopOn ⁡ B
14 12 3 13 syl2anc ⊢ φ → TopOpen ⁡ R qTop F ∈ TopOn ⁡ B
15 1 2 3 4 imasbas ⊢ φ → B = Base U
16 15 fveq2d ⊢ φ → TopOn ⁡ B = TopOn ⁡ Base U
17 14 16 eleqtrd ⊢ φ → TopOpen ⁡ R qTop F ∈ TopOn ⁡ Base U
18 7 17 eqeltrd ⊢ φ → TopOpen ⁡ U ∈ TopOn ⁡ Base U
19 eqid ⊢ Base U = Base U
20 19 6 istps ⊢ U ∈ TopSp ↔ TopOpen ⁡ U ∈ TopOn ⁡ Base U
21 18 20 sylibr ⊢ φ → U ∈ TopSp