Metamath Proof Explorer

Theorem qtoptop2

Description: The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Assertion qtoptop2 
|- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop F ) e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 qtopres 
 |-  ( F e. V -> ( J qTop F ) = ( J qTop ( F |` U. J ) ) )
3 2 3ad2ant2 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop F ) = ( J qTop ( F |` U. J ) ) )
4 simp1 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> J e. Top )
5 funres 
 |-  ( Fun F -> Fun ( F |` U. J ) )
6 5 3ad2ant3 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> Fun ( F |` U. J ) )
7 funforn 
 |-  ( Fun ( F |` U. J ) <-> ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) )
8 6 7 sylib 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) )
9 dmres 
 |-  dom ( F |` U. J ) = ( U. J i^i dom F )
10 inss1 
 |-  ( U. J i^i dom F ) C_ U. J
11 9 10 eqsstri 
 |-  dom ( F |` U. J ) C_ U. J
12 11 a1i 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> dom ( F |` U. J ) C_ U. J )
13 1 elqtop 
 |-  ( ( J e. Top /\ ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) /\ dom ( F |` U. J ) C_ U. J ) -> ( y e. ( J qTop ( F |` U. J ) ) <-> ( y C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " y ) e. J ) ) )
14 4 8 12 13 syl3anc 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( y e. ( J qTop ( F |` U. J ) ) <-> ( y C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " y ) e. J ) ) )
15 14 simprbda 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ y e. ( J qTop ( F |` U. J ) ) ) -> y C_ ran ( F |` U. J ) )
16 velpw 
 |-  ( y e. ~P ran ( F |` U. J ) <-> y C_ ran ( F |` U. J ) )
17 15 16 sylibr 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ y e. ( J qTop ( F |` U. J ) ) ) -> y e. ~P ran ( F |` U. J ) )
18 17 ex 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( y e. ( J qTop ( F |` U. J ) ) -> y e. ~P ran ( F |` U. J ) ) )
19 18 ssrdv 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop ( F |` U. J ) ) C_ ~P ran ( F |` U. J ) )
20 sstr2 
 |-  ( x C_ ( J qTop ( F |` U. J ) ) -> ( ( J qTop ( F |` U. J ) ) C_ ~P ran ( F |` U. J ) -> x C_ ~P ran ( F |` U. J ) ) )
21 19 20 syl5com 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> x C_ ~P ran ( F |` U. J ) ) )
22 sspwuni 
 |-  ( x C_ ~P ran ( F |` U. J ) <-> U. x C_ ran ( F |` U. J ) )
23 21 22 syl6ib 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> U. x C_ ran ( F |` U. J ) ) )
24 imauni 
 |-  ( `' ( F |` U. J ) " U. x ) = U_ y e. x ( `' ( F |` U. J ) " y )
25 14 simplbda 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ y e. ( J qTop ( F |` U. J ) ) ) -> ( `' ( F |` U. J ) " y ) e. J )
26 25 ralrimiva 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> A. y e. ( J qTop ( F |` U. J ) ) ( `' ( F |` U. J ) " y ) e. J )
27 ssralv 
 |-  ( x C_ ( J qTop ( F |` U. J ) ) -> ( A. y e. ( J qTop ( F |` U. J ) ) ( `' ( F |` U. J ) " y ) e. J -> A. y e. x ( `' ( F |` U. J ) " y ) e. J ) )
28 26 27 mpan9 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ x C_ ( J qTop ( F |` U. J ) ) ) -> A. y e. x ( `' ( F |` U. J ) " y ) e. J )
29 iunopn 
 |-  ( ( J e. Top /\ A. y e. x ( `' ( F |` U. J ) " y ) e. J ) -> U_ y e. x ( `' ( F |` U. J ) " y ) e. J )
30 4 28 29 syl2an2r 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ x C_ ( J qTop ( F |` U. J ) ) ) -> U_ y e. x ( `' ( F |` U. J ) " y ) e. J )
31 24 30 eqeltrid 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ x C_ ( J qTop ( F |` U. J ) ) ) -> ( `' ( F |` U. J ) " U. x ) e. J )
32 31 ex 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> ( `' ( F |` U. J ) " U. x ) e. J ) )
33 23 32 jcad 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> ( U. x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " U. x ) e. J ) ) )
34 1 elqtop 
 |-  ( ( J e. Top /\ ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) /\ dom ( F |` U. J ) C_ U. J ) -> ( U. x e. ( J qTop ( F |` U. J ) ) <-> ( U. x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " U. x ) e. J ) ) )
35 4 8 12 34 syl3anc 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( U. x e. ( J qTop ( F |` U. J ) ) <-> ( U. x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " U. x ) e. J ) ) )
36 33 35 sylibrd 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> U. x e. ( J qTop ( F |` U. J ) ) ) )
37 36 alrimiv 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> A. x ( x C_ ( J qTop ( F |` U. J ) ) -> U. x e. ( J qTop ( F |` U. J ) ) ) )
38 inss1 
 |-  ( x i^i y ) C_ x
39 1 elqtop 
 |-  ( ( J e. Top /\ ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) /\ dom ( F |` U. J ) C_ U. J ) -> ( x e. ( J qTop ( F |` U. J ) ) <-> ( x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " x ) e. J ) ) )
40 4 8 12 39 syl3anc 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x e. ( J qTop ( F |` U. J ) ) <-> ( x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " x ) e. J ) ) )
41 40 biimpa 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ x e. ( J qTop ( F |` U. J ) ) ) -> ( x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " x ) e. J ) )
42 41 adantrr 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " x ) e. J ) )
43 42 simpld 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> x C_ ran ( F |` U. J ) )
44 38 43 sstrid 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( x i^i y ) C_ ran ( F |` U. J ) )
45 6 adantr 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> Fun ( F |` U. J ) )
46 inpreima 
 |-  ( Fun ( F |` U. J ) -> ( `' ( F |` U. J ) " ( x i^i y ) ) = ( ( `' ( F |` U. J ) " x ) i^i ( `' ( F |` U. J ) " y ) ) )
47 45 46 syl 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( `' ( F |` U. J ) " ( x i^i y ) ) = ( ( `' ( F |` U. J ) " x ) i^i ( `' ( F |` U. J ) " y ) ) )
48 4 adantr 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> J e. Top )
49 42 simprd 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( `' ( F |` U. J ) " x ) e. J )
50 25 adantrl 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( `' ( F |` U. J ) " y ) e. J )
51 inopn 
 |-  ( ( J e. Top /\ ( `' ( F |` U. J ) " x ) e. J /\ ( `' ( F |` U. J ) " y ) e. J ) -> ( ( `' ( F |` U. J ) " x ) i^i ( `' ( F |` U. J ) " y ) ) e. J )
52 48 49 50 51 syl3anc 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( ( `' ( F |` U. J ) " x ) i^i ( `' ( F |` U. J ) " y ) ) e. J )
53 47 52 eqeltrd 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( `' ( F |` U. J ) " ( x i^i y ) ) e. J )
54 1 elqtop 
 |-  ( ( J e. Top /\ ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) /\ dom ( F |` U. J ) C_ U. J ) -> ( ( x i^i y ) e. ( J qTop ( F |` U. J ) ) <-> ( ( x i^i y ) C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " ( x i^i y ) ) e. J ) ) )
55 4 8 12 54 syl3anc 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( ( x i^i y ) e. ( J qTop ( F |` U. J ) ) <-> ( ( x i^i y ) C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " ( x i^i y ) ) e. J ) ) )
56 55 adantr 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( ( x i^i y ) e. ( J qTop ( F |` U. J ) ) <-> ( ( x i^i y ) C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " ( x i^i y ) ) e. J ) ) )
57 44 53 56 mpbir2and 
 |-  ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( x i^i y ) e. ( J qTop ( F |` U. J ) ) )
58 57 ralrimivva 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> A. x e. ( J qTop ( F |` U. J ) ) A. y e. ( J qTop ( F |` U. J ) ) ( x i^i y ) e. ( J qTop ( F |` U. J ) ) )
59 ovex 
 |-  ( J qTop ( F |` U. J ) ) e. _V
60 istopg 
 |-  ( ( J qTop ( F |` U. J ) ) e. _V -> ( ( J qTop ( F |` U. J ) ) e. Top <-> ( A. x ( x C_ ( J qTop ( F |` U. J ) ) -> U. x e. ( J qTop ( F |` U. J ) ) ) /\ A. x e. ( J qTop ( F |` U. J ) ) A. y e. ( J qTop ( F |` U. J ) ) ( x i^i y ) e. ( J qTop ( F |` U. J ) ) ) ) )
61 59 60 ax-mp 
 |-  ( ( J qTop ( F |` U. J ) ) e. Top <-> ( A. x ( x C_ ( J qTop ( F |` U. J ) ) -> U. x e. ( J qTop ( F |` U. J ) ) ) /\ A. x e. ( J qTop ( F |` U. J ) ) A. y e. ( J qTop ( F |` U. J ) ) ( x i^i y ) e. ( J qTop ( F |` U. J ) ) ) )
62 37 58 61 sylanbrc 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop ( F |` U. J ) ) e. Top )
63 3 62 eqeltrd 
 |-  ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop F ) e. Top )