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 
|- ( ph -> U = ( F "s R ) )
imastps.v 
|- ( ph -> V = ( Base ` R ) )
imastps.f 
|- ( ph -> F : V -onto-> B )
imastps.r 
|- ( ph -> R e. TopSp )
Assertion imastps 
|- ( ph -> U e. TopSp )

Proof

Step Hyp Ref Expression
1 imastps.u 
 |-  ( ph -> U = ( F "s R ) )
2 imastps.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imastps.f 
 |-  ( ph -> F : V -onto-> B )
4 imastps.r 
 |-  ( ph -> R e. TopSp )
5 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
6 eqid 
 |-  ( TopOpen ` U ) = ( TopOpen ` U )
7 1 2 3 4 5 6 imastopn 
 |-  ( ph -> ( TopOpen ` U ) = ( ( TopOpen ` R ) qTop F ) )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 8 5 istps 
 |-  ( R e. TopSp <-> ( TopOpen ` R ) e. ( TopOn ` ( Base ` R ) ) )
10 4 9 sylib 
 |-  ( ph -> ( TopOpen ` R ) e. ( TopOn ` ( Base ` R ) ) )
11 2 fveq2d 
 |-  ( ph -> ( TopOn ` V ) = ( TopOn ` ( Base ` R ) ) )
12 10 11 eleqtrrd 
 |-  ( ph -> ( TopOpen ` R ) e. ( TopOn ` V ) )
13 qtoptopon 
 |-  ( ( ( TopOpen ` R ) e. ( TopOn ` V ) /\ F : V -onto-> B ) -> ( ( TopOpen ` R ) qTop F ) e. ( TopOn ` B ) )
14 12 3 13 syl2anc 
 |-  ( ph -> ( ( TopOpen ` R ) qTop F ) e. ( TopOn ` B ) )
15 1 2 3 4 imasbas 
 |-  ( ph -> B = ( Base ` U ) )
16 15 fveq2d 
 |-  ( ph -> ( TopOn ` B ) = ( TopOn ` ( Base ` U ) ) )
17 14 16 eleqtrd 
 |-  ( ph -> ( ( TopOpen ` R ) qTop F ) e. ( TopOn ` ( Base ` U ) ) )
18 7 17 eqeltrd 
 |-  ( ph -> ( TopOpen ` U ) e. ( TopOn ` ( Base ` U ) ) )
19 eqid 
 |-  ( Base ` U ) = ( Base ` U )
20 19 6 istps 
 |-  ( U e. TopSp <-> ( TopOpen ` U ) e. ( TopOn ` ( Base ` U ) ) )
21 18 20 sylibr 
 |-  ( ph -> U e. TopSp )