Metamath Proof Explorer

Theorem imastopn

Description: The topology of an image structure. (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 )
imastopn.r 
|- ( ph -> R e. W )
imastopn.j 
|- J = ( TopOpen ` R )
imastopn.o 
|- O = ( TopOpen ` U )
Assertion imastopn 
|- ( ph -> O = ( J qTop F ) )

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 imastopn.r 
 |-  ( ph -> R e. W )
5 imastopn.j 
 |-  J = ( TopOpen ` R )
6 imastopn.o 
 |-  O = ( TopOpen ` U )
7 eqid 
 |-  ( TopSet ` U ) = ( TopSet ` U )
8 1 2 3 4 5 7 imastset 
 |-  ( ph -> ( TopSet ` U ) = ( J qTop F ) )
9 5 fvexi 
 |-  J e. _V
10 fofn 
 |-  ( F : V -onto-> B -> F Fn V )
11 3 10 syl 
 |-  ( ph -> F Fn V )
12 fvex 
 |-  ( Base ` R ) e. _V
13 2 12 eqeltrdi 
 |-  ( ph -> V e. _V )
14 fnex 
 |-  ( ( F Fn V /\ V e. _V ) -> F e. _V )
15 11 13 14 syl2anc 
 |-  ( ph -> F e. _V )
16 eqid 
 |-  U. J = U. J
17 16 qtopval 
 |-  ( ( J e. _V /\ F e. _V ) -> ( J qTop F ) = { x e. ~P ( F " U. J ) | ( ( `' F " x ) i^i U. J ) e. J } )
18 9 15 17 sylancr 
 |-  ( ph -> ( J qTop F ) = { x e. ~P ( F " U. J ) | ( ( `' F " x ) i^i U. J ) e. J } )
19 8 18 eqtrd 
 |-  ( ph -> ( TopSet ` U ) = { x e. ~P ( F " U. J ) | ( ( `' F " x ) i^i U. J ) e. J } )
20 ssrab2 
 |-  { x e. ~P ( F " U. J ) | ( ( `' F " x ) i^i U. J ) e. J } C_ ~P ( F " U. J )
21 imassrn 
 |-  ( F " U. J ) C_ ran F
22 forn 
 |-  ( F : V -onto-> B -> ran F = B )
23 3 22 syl 
 |-  ( ph -> ran F = B )
24 1 2 3 4 imasbas 
 |-  ( ph -> B = ( Base ` U ) )
25 23 24 eqtrd 
 |-  ( ph -> ran F = ( Base ` U ) )
26 21 25 sseqtrid 
 |-  ( ph -> ( F " U. J ) C_ ( Base ` U ) )
27 26 sspwd 
 |-  ( ph -> ~P ( F " U. J ) C_ ~P ( Base ` U ) )
28 20 27 sstrid 
 |-  ( ph -> { x e. ~P ( F " U. J ) | ( ( `' F " x ) i^i U. J ) e. J } C_ ~P ( Base ` U ) )
29 19 28 eqsstrd 
 |-  ( ph -> ( TopSet ` U ) C_ ~P ( Base ` U ) )
30 eqid 
 |-  ( Base ` U ) = ( Base ` U )
31 30 7 topnid 
 |-  ( ( TopSet ` U ) C_ ~P ( Base ` U ) -> ( TopSet ` U ) = ( TopOpen ` U ) )
32 29 31 syl 
 |-  ( ph -> ( TopSet ` U ) = ( TopOpen ` U ) )
33 32 6 eqtr4di 
 |-  ( ph -> ( TopSet ` U ) = O )
34 33 8 eqtr3d 
 |-  ( ph -> O = ( J qTop F ) )