MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  qtoptop2 Unicode version

Theorem qtoptop2 17654
Description: The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
Assertion
Ref Expression
qtoptop2  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( J qTop  F )  e.  Top )

Proof of Theorem qtoptop2
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2389 . . . 4  |-  U. J  =  U. J
21qtopres 17653 . . 3  |-  ( F  e.  V  ->  ( J qTop  F )  =  ( J qTop  ( F  |`  U. J ) ) )
323ad2ant2 979 . 2  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( J qTop  F )  =  ( J qTop  ( F  |`  U. J ) ) )
4 simp1 957 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  J  e.  Top )
5 funres 5434 . . . . . . . . . . . . . . 15  |-  ( Fun 
F  ->  Fun  ( F  |`  U. J ) )
653ad2ant3 980 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  Fun  ( F  |`  U. J
) )
7 funforn 5602 . . . . . . . . . . . . . 14  |-  ( Fun  ( F  |`  U. J
)  <->  ( F  |`  U. J ) : dom  ( F  |`  U. J
) -onto-> ran  ( F  |`  U. J ) )
86, 7sylib 189 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( F  |`  U. J ) : dom  ( F  |`  U. J ) -onto-> ran  ( F  |`  U. J
) )
9 dmres 5109 . . . . . . . . . . . . . . 15  |-  dom  ( F  |`  U. J )  =  ( U. J  i^i  dom  F )
10 inss1 3506 . . . . . . . . . . . . . . 15  |-  ( U. J  i^i  dom  F )  C_ 
U. J
119, 10eqsstri 3323 . . . . . . . . . . . . . 14  |-  dom  ( F  |`  U. J ) 
C_  U. J
1211a1i 11 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  dom  ( F  |`  U. J
)  C_  U. J )
131elqtop 17652 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) )
144, 8, 12, 13syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
1514simprbda 607 . . . . . . . . . . 11  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  y  e.  ( J qTop  ( F  |`  U. J ) ) )  ->  y  C_  ran  ( F  |`  U. J
) )
16 vex 2904 . . . . . . . . . . . 12  |-  y  e. 
_V
1716elpw 3750 . . . . . . . . . . 11  |-  ( y  e.  ~P ran  ( F  |`  U. J )  <-> 
y  C_  ran  ( F  |`  U. J ) )
1815, 17sylibr 204 . . . . . . . . . 10  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  y  e.  ( J qTop  ( F  |`  U. J ) ) )  ->  y  e.  ~P ran  ( F  |`  U. J ) )
1918ex 424 . . . . . . . . 9  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  (
y  e.  ( J qTop  ( F  |`  U. J
) )  ->  y  e.  ~P ran  ( F  |`  U. J ) ) )
2019ssrdv 3299 . . . . . . . 8  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( J qTop  ( F  |`  U. J
) )  C_  ~P ran  ( F  |`  U. J
) )
21 sstr2 3300 . . . . . . . 8  |-  ( 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
) ) )
2220, 21syl5com 28 . . . . . . 7  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  (
x  C_  ( J qTop  ( F  |`  U. J
) )  ->  x  C_ 
~P ran  ( F  |` 
U. J ) ) )
23 sspwuni 4119 . . . . . . 7  |-  ( x 
C_  ~P ran  ( F  |`  U. J )  <->  U. x  C_ 
ran  ( F  |`  U. J ) )
2422, 23syl6ib 218 . . . . . 6  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  (
x  C_  ( J qTop  ( F  |`  U. J
) )  ->  U. x  C_ 
ran  ( F  |`  U. J ) ) )
25 imauni 5934 . . . . . . . 8  |-  ( `' ( F  |`  U. J
) " U. x
)  =  U_ y  e.  x  ( `' ( F  |`  U. J
) " y )
26 simpl1 960 . . . . . . . . 9  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  x  C_  ( J qTop  ( F  |`  U. J ) ) )  ->  J  e.  Top )
2714simplbda 608 . . . . . . . . . . 11  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  y  e.  ( J qTop  ( F  |`  U. J ) ) )  ->  ( `' ( F  |`  U. J
) " y )  e.  J )
2827ralrimiva 2734 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  A. y  e.  ( J qTop  ( F  |`  U. J ) ) ( `' ( F  |`  U. J ) "
y )  e.  J
)
29 ssralv 3352 . . . . . . . . . 10  |-  ( 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 ) )
3028, 29mpan9 456 . . . . . . . . 9  |-  ( ( ( 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 )
31 iunopn 16896 . . . . . . . . 9  |-  ( ( J  e.  Top  /\  A. y  e.  x  ( `' ( F  |`  U. J ) " y
)  e.  J )  ->  U_ y  e.  x  ( `' ( F  |`  U. J ) " y
)  e.  J )
3226, 30, 31syl2anc 643 . . . . . . . 8  |-  ( ( ( 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 )
3325, 32syl5eqel 2473 . . . . . . 7  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  x  C_  ( J qTop  ( F  |`  U. J ) ) )  ->  ( `' ( F  |`  U. J
) " U. x
)  e.  J )
3433ex 424 . . . . . 6  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  (
x  C_  ( J qTop  ( F  |`  U. J
) )  ->  ( `' ( F  |`  U. J ) " U. x )  e.  J
) )
3524, 34jcad 520 . . . . 5  |-  ( ( 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 ) ) )
361elqtop 17652 . . . . . 6  |-  ( ( 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 ) ) )
374, 8, 12, 36syl3anc 1184 . . . . 5  |-  ( ( 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
) ) )
3835, 37sylibrd 226 . . . 4  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  (
x  C_  ( J qTop  ( F  |`  U. J
) )  ->  U. x  e.  ( J qTop  ( F  |`  U. J ) ) ) )
3938alrimiv 1638 . . 3  |-  ( ( 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 ) ) ) )
40 inss1 3506 . . . . . 6  |-  ( x  i^i  y )  C_  x
411elqtop 17652 . . . . . . . . . 10  |-  ( ( 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 ) ) )
424, 8, 12, 41syl3anc 1184 . . . . . . . . 9  |-  ( ( 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 ) ) )
4342biimpa 471 . . . . . . . 8  |-  ( ( ( 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 ) )
4443adantrr 698 . . . . . . 7  |-  ( ( ( 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 ) )
4544simpld 446 . . . . . 6  |-  ( ( ( 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 ) )
4640, 45syl5ss 3304 . . . . 5  |-  ( ( ( 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 ) )
476adantr 452 . . . . . . 7  |-  ( ( ( 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
) )
48 inpreima 5798 . . . . . . 7  |-  ( Fun  ( F  |`  U. J
)  ->  ( `' ( F  |`  U. J
) " ( x  i^i  y ) )  =  ( ( `' ( F  |`  U. J
) " x )  i^i  ( `' ( F  |`  U. J )
" y ) ) )
4947, 48syl 16 . . . . . 6  |-  ( ( ( 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 ) ) )
504adantr 452 . . . . . . 7  |-  ( ( ( 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 )
5144simprd 450 . . . . . . 7  |-  ( ( ( 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 )
5227adantrl 697 . . . . . . 7  |-  ( ( ( 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 )
53 inopn 16897 . . . . . . 7  |-  ( ( 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 )
5450, 51, 52, 53syl3anc 1184 . . . . . 6  |-  ( ( ( 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
)
5549, 54eqeltrd 2463 . . . . 5  |-  ( ( ( 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 )
561elqtop 17652 . . . . . . 7  |-  ( ( 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 ) ) )
574, 8, 12, 56syl3anc 1184 . . . . . 6  |-  ( ( 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 ) ) )
5857adantr 452 . . . . 5  |-  ( ( ( 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 ) ) )
5946, 55, 58mpbir2and 889 . . . 4  |-  ( ( ( 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 ) ) )
6059ralrimivva 2743 . . 3  |-  ( ( 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 ) ) )
61 ovex 6047 . . . 4  |-  ( J qTop  ( F  |`  U. J
) )  e.  _V
62 istopg 16893 . . . 4  |-  ( ( 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 ) ) ) ) )
6361, 62ax-mp 8 . . 3  |-  ( ( 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 ) ) ) )
6439, 60, 63sylanbrc 646 . 2  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( J qTop  ( F  |`  U. J
) )  e.  Top )
653, 64eqeltrd 2463 1  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( J qTop  F )  e.  Top )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936   A.wal 1546    = wceq 1649    e. wcel 1717   A.wral 2651   _Vcvv 2901    i^i cin 3264    C_ wss 3265   ~Pcpw 3744   U.cuni 3959   U_ciun 4037   `'ccnv 4819   dom cdm 4820   ran crn 4821    |` cres 4822   "cima 4823   Fun wfun 5390   -onto->wfo 5394  (class class class)co 6022   qTop cqtop 13658   Topctop 16883
This theorem is referenced by:  qtoptop  17655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-rep 4263  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-reu 2658  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-qtop 13662  df-top 16888
  Copyright terms: Public domain W3C validator