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 )