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

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 ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imastps.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imastps.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imastps.r ⊢ ( 𝜑 → 𝑅 ∈ TopSp )
Assertion imastps ( 𝜑 → 𝑈 ∈ TopSp )

Proof

Step Hyp Ref Expression
1 imastps.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imastps.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imastps.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4 imastps.r ⊢ ( 𝜑 → 𝑅 ∈ TopSp )
5 eqid ⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
6 eqid ⊢ ( TopOpen ‘ 𝑈 ) = ( TopOpen ‘ 𝑈 )
7 1 2 3 4 5 6 imastopn ⊢ ( 𝜑 → ( TopOpen ‘ 𝑈 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 8 5 istps ⊢ ( 𝑅 ∈ TopSp ↔ ( TopOpen ‘ 𝑅 ) ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
10 4 9 sylib ⊢ ( 𝜑 → ( TopOpen ‘ 𝑅 ) ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
11 2 fveq2d ⊢ ( 𝜑 → ( TopOn ‘ 𝑉 ) = ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
12 10 11 eleqtrrd ⊢ ( 𝜑 → ( TopOpen ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑉 ) )
13 qtoptopon ⊢ ( ( ( TopOpen ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑉 ) ∧ 𝐹 : 𝑉 –onto→ 𝐵 ) → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ∈ ( TopOn ‘ 𝐵 ) )
14 12 3 13 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ∈ ( TopOn ‘ 𝐵 ) )
15 1 2 3 4 imasbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
16 15 fveq2d ⊢ ( 𝜑 → ( TopOn ‘ 𝐵 ) = ( TopOn ‘ ( Base ‘ 𝑈 ) ) )
17 14 16 eleqtrd ⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ∈ ( TopOn ‘ ( Base ‘ 𝑈 ) ) )
18 7 17 eqeltrd ⊢ ( 𝜑 → ( TopOpen ‘ 𝑈 ) ∈ ( TopOn ‘ ( Base ‘ 𝑈 ) ) )
19 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
20 19 6 istps ⊢ ( 𝑈 ∈ TopSp ↔ ( TopOpen ‘ 𝑈 ) ∈ ( TopOn ‘ ( Base ‘ 𝑈 ) ) )
21 18 20 sylibr ⊢ ( 𝜑 → 𝑈 ∈ TopSp )