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

Theorem qtoptop2 17392
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 2285 . . . 4  |-  U. J  =  U. J
21qtopres 17391 . . 3  |-  ( F  e.  V  ->  ( J qTop  F )  =  ( J qTop  ( F  |`  U. J ) ) )
323ad2ant2 977 . 2  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( J qTop  F )  =  ( J qTop  ( F  |`  U. J ) ) )
4 simp1 955 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  J  e.  Top )
5 funres 5295 . . . . . . . . . . . . . . 15  |-  ( Fun 
F  ->  Fun  ( F  |`  U. J ) )
653ad2ant3 978 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  Fun  ( F  |`  U. J
) )
7 funforn 5460 . . . . . . . . . . . . . 14  |-  ( Fun  ( F  |`  U. J
)  <->  ( F  |`  U. J ) : dom  ( F  |`  U. J
) -onto-> ran  ( F  |`  U. J ) )
86, 7sylib 188 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( F  |`  U. J ) : dom  ( F  |`  U. J ) -onto-> ran  ( F  |`  U. J
) )
9 dmres 4978 . . . . . . . . . . . . . . 15  |-  dom  ( F  |`  U. J )  =  ( U. J  i^i  dom  F )
10 inss1 3391 . . . . . . . . . . . . . . 15  |-  ( U. J  i^i  dom  F )  C_ 
U. J
119, 10eqsstri 3210 . . . . . . . . . . . . . 14  |-  dom  ( F  |`  U. J ) 
C_  U. J
1211a1i 10 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  dom  ( F  |`  U. J
)  C_  U. J )
131elqtop 17390 . . . . . . . . . . . . 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 1182 . . . . . . . . . . . 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 606 . . . . . . . . . . 11  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  y  e.  ( J qTop  ( F  |`  U. J ) ) )  ->  y  C_  ran  ( F  |`  U. J
) )
16 vex 2793 . . . . . . . . . . . 12  |-  y  e. 
_V
1716elpw 3633 . . . . . . . . . . 11  |-  ( y  e.  ~P ran  ( F  |`  U. J )  <-> 
y  C_  ran  ( F  |`  U. J ) )
1815, 17sylibr 203 . . . . . . . . . 10  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  y  e.  ( J qTop  ( F  |`  U. J ) ) )  ->  y  e.  ~P ran  ( F  |`  U. J ) )
1918ex 423 . . . . . . . . 9  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  (
y  e.  ( J qTop  ( F  |`  U. J
) )  ->  y  e.  ~P ran  ( F  |`  U. J ) ) )
2019ssrdv 3187 . . . . . . . 8  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( J qTop  ( F  |`  U. J
) )  C_  ~P ran  ( F  |`  U. J
) )
21 sstr2 3188 . . . . . . . 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 26 . . . . . . 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 3989 . . . . . . 7  |-  ( x 
C_  ~P ran  ( F  |`  U. J )  <->  U. x  C_ 
ran  ( F  |`  U. J ) )
2422, 23syl6ib 217 . . . . . 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 5774 . . . . . . . 8  |-  ( `' ( F  |`  U. J
) " U. x
)  =  U_ y  e.  x  ( `' ( F  |`  U. J
) " y )
26 simpl1 958 . . . . . . . . 9  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  x  C_  ( J qTop  ( F  |`  U. J ) ) )  ->  J  e.  Top )
2714simplbda 607 . . . . . . . . . . 11  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  y  e.  ( J qTop  ( F  |`  U. J ) ) )  ->  ( `' ( F  |`  U. J
) " y )  e.  J )
2827ralrimiva 2628 . . . . . . . . . 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 3239 . . . . . . . . . 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 455 . . . . . . . . 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 16646 . . . . . . . . 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 642 . . . . . . . 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 2369 . . . . . . 7  |-  ( ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  /\  x  C_  ( J qTop  ( F  |`  U. J ) ) )  ->  ( `' ( F  |`  U. J
) " U. x
)  e.  J )
3433ex 423 . . . . . 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 519 . . . . 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 17390 . . . . . 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 1182 . . . . 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 225 . . . 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 1619 . . 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 3391 . . . . . 6  |-  ( x  i^i  y )  C_  x
411elqtop 17390 . . . . . . . . . 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 1182 . . . . . . . . 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 470 . . . . . . . 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 697 . . . . . . 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 445 . . . . . 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 3192 . . . . 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 451 . . . . . . 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 5654 . . . . . . 7  |-  ( Fun  ( F  |`  U. J
)  ->  ( `' ( F  |`  U. J
) " ( x  i^i  y ) )  =  ( ( `' ( F  |`  U. J
) " x )  i^i  ( `' ( F  |`  U. J )
" y ) ) )
4947, 48syl 15 . . . . . 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 451 . . . . . . 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 449 . . . . . . 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 696 . . . . . . 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 16647 . . . . . . 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 1182 . . . . . 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 2359 . . . . 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 17390 . . . . . . 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 1182 . . . . . 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 451 . . . . 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 888 . . . 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 2637 . . 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 5885 . . . 4  |-  ( J qTop  ( F  |`  U. J
) )  e.  _V
62 istopg 16643 . . . 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 645 . 2  |-  ( ( J  e.  Top  /\  F  e.  V  /\  Fun  F )  ->  ( J qTop  ( F  |`  U. J
) )  e.  Top )
653, 64eqeltrd 2359 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 176    /\ wa 358    /\ w3a 934   A.wal 1529    = wceq 1625    e. wcel 1686   A.wral 2545   _Vcvv 2790    i^i cin 3153    C_ wss 3154   ~Pcpw 3627   U.cuni 3829   U_ciun 3907   `'ccnv 4690   dom cdm 4691   ran crn 4692    |` cres 4693   "cima 4694   Fun wfun 5251   -onto->wfo 5255  (class class class)co 5860   qTop cqtop 13408   Topctop 16633
This theorem is referenced by:  qtoptop  17393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-qtop 13412  df-top 16638
  Copyright terms: Public domain W3C validator