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

Theorem tgqtop 17665
Description: An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015.)
Hypothesis
Ref Expression
qtopcmp.1  |-  X  = 
U. J
Assertion
Ref Expression
tgqtop  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
( topGen `  J ) qTop  F )  =  ( topGen `  ( J qTop  F ) ) )

Proof of Theorem tgqtop
Dummy variables  x  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1ocnv 5627 . . . . . . . . 9  |-  ( F : X -1-1-onto-> Y  ->  `' F : Y -1-1-onto-> X )
2 f1ofun 5616 . . . . . . . . 9  |-  ( `' F : Y -1-1-onto-> X  ->  Fun  `' F )
31, 2syl 16 . . . . . . . 8  |-  ( F : X -1-1-onto-> Y  ->  Fun  `' F
)
43ad2antlr 708 . . . . . . 7  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  Fun  `' F )
5 simpr 448 . . . . . . . 8  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  x  C_  Y )
6 df-rn 4829 . . . . . . . . 9  |-  ran  F  =  dom  `' F
7 f1ofo 5621 . . . . . . . . . . 11  |-  ( F : X -1-1-onto-> Y  ->  F : X -onto-> Y )
87ad2antlr 708 . . . . . . . . . 10  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  F : X -onto-> Y )
9 forn 5596 . . . . . . . . . 10  |-  ( F : X -onto-> Y  ->  ran  F  =  Y )
108, 9syl 16 . . . . . . . . 9  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  ran  F  =  Y )
116, 10syl5eqr 2433 . . . . . . . 8  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  dom  `' F  =  Y )
125, 11sseqtr4d 3328 . . . . . . 7  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  x  C_ 
dom  `' F )
13 funimass4 5716 . . . . . . 7  |-  ( ( Fun  `' F  /\  x  C_  dom  `' F
)  ->  ( ( `' F " x ) 
C_  U. ( J  i^i  ~P ( `' F "
x ) )  <->  A. y  e.  x  ( `' F `  y )  e.  U. ( J  i^i  ~P ( `' F "
x ) ) ) )
144, 12, 13syl2anc 643 . . . . . 6  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  (
( `' F "
x )  C_  U. ( J  i^i  ~P ( `' F " x ) )  <->  A. y  e.  x  ( `' F `  y )  e.  U. ( J  i^i  ~P ( `' F " x ) ) ) )
15 dfss3 3281 . . . . . . 7  |-  ( x 
C_  U. ( ( J qTop 
F )  i^i  ~P x )  <->  A. y  e.  x  y  e.  U. ( ( J qTop  F
)  i^i  ~P x
) )
16 inss1 3504 . . . . . . . . . . . . . . . 16  |-  ( ( J qTop  F )  i^i 
~P x )  C_  ( J qTop  F )
17 simprl 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  z  e.  ( ( J qTop  F
)  i^i  ~P x
) )
1816, 17sseldi 3289 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  z  e.  ( J qTop  F )
)
19 qtopcmp.1 . . . . . . . . . . . . . . . . . 18  |-  X  = 
U. J
2019elqtop2 17654 . . . . . . . . . . . . . . . . 17  |-  ( ( J  e.  TopBases  /\  F : X -onto-> Y )  ->  (
z  e.  ( J qTop 
F )  <->  ( z  C_  Y  /\  ( `' F " z )  e.  J ) ) )
217, 20sylan2 461 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
z  e.  ( J qTop 
F )  <->  ( z  C_  Y  /\  ( `' F " z )  e.  J ) ) )
2221ad3antrrr 711 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  ( z  e.  ( J qTop  F )  <-> 
( z  C_  Y  /\  ( `' F "
z )  e.  J
) ) )
2318, 22mpbid 202 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  ( z  C_  Y  /\  ( `' F " z )  e.  J ) )
2423simprd 450 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  ( `' F " z )  e.  J )
25 inss2 3505 . . . . . . . . . . . . . . . . 17  |-  ( ( J qTop  F )  i^i 
~P x )  C_  ~P x
2625, 17sseldi 3289 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  z  e.  ~P x )
2726elpwid 3751 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  z  C_  x )
28 imass2 5180 . . . . . . . . . . . . . . 15  |-  ( z 
C_  x  ->  ( `' F " z ) 
C_  ( `' F " x ) )
2927, 28syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  ( `' F " z )  C_  ( `' F " x ) )
30 elpwg 3749 . . . . . . . . . . . . . . 15  |-  ( ( `' F " z )  e.  J  ->  (
( `' F "
z )  e.  ~P ( `' F " x )  <-> 
( `' F "
z )  C_  ( `' F " x ) ) )
3124, 30syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  ( ( `' F " z )  e.  ~P ( `' F " x )  <-> 
( `' F "
z )  C_  ( `' F " x ) ) )
3229, 31mpbird 224 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  ( `' F " z )  e. 
~P ( `' F " x ) )
33 elin 3473 . . . . . . . . . . . . 13  |-  ( ( `' F " z )  e.  ( J  i^i  ~P ( `' F "
x ) )  <->  ( ( `' F " z )  e.  J  /\  ( `' F " z )  e.  ~P ( `' F " x ) ) )
3424, 32, 33sylanbrc 646 . . . . . . . . . . . 12  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  ( `' F " z )  e.  ( J  i^i  ~P ( `' F " x ) ) )
35 simp-4r 744 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  F : X
-1-1-onto-> Y )
3635, 1syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  `' F : Y -1-1-onto-> X )
37 f1ofn 5615 . . . . . . . . . . . . . 14  |-  ( `' F : Y -1-1-onto-> X  ->  `' F  Fn  Y
)
3836, 37syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  `' F  Fn  Y )
395ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  x  C_  Y
)
4027, 39sstrd 3301 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  z  C_  Y )
41 simprr 734 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  y  e.  z )
42 fnfvima 5915 . . . . . . . . . . . . 13  |-  ( ( `' F  Fn  Y  /\  z  C_  Y  /\  y  e.  z )  ->  ( `' F `  y )  e.  ( `' F " z ) )
4338, 40, 41, 42syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  ( `' F `  y )  e.  ( `' F "
z ) )
44 eleq2 2448 . . . . . . . . . . . . 13  |-  ( w  =  ( `' F " z )  ->  (
( `' F `  y )  e.  w  <->  ( `' F `  y )  e.  ( `' F " z ) ) )
4544rspcev 2995 . . . . . . . . . . . 12  |-  ( ( ( `' F "
z )  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  ( `' F " z ) )  ->  E. w  e.  ( J  i^i  ~P ( `' F " x ) ) ( `' F `  y )  e.  w
)
4634, 43, 45syl2anc 643 . . . . . . . . . . 11  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
z  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  z )
)  ->  E. w  e.  ( J  i^i  ~P ( `' F " x ) ) ( `' F `  y )  e.  w
)
4746rexlimdvaa 2774 . . . . . . . . . 10  |-  ( ( ( ( J  e.  TopBases 
/\  F : X -1-1-onto-> Y
)  /\  x  C_  Y
)  /\  y  e.  x )  ->  ( E. z  e.  (
( J qTop  F )  i^i  ~P x ) y  e.  z  ->  E. w  e.  ( J  i^i  ~P ( `' F " x ) ) ( `' F `  y )  e.  w
) )
48 simp-4r 744 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  F : X -1-1-onto-> Y
)
49 f1ofun 5616 . . . . . . . . . . . . . . . . 17  |-  ( F : X -1-1-onto-> Y  ->  Fun  F )
5048, 49syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  Fun  F )
51 inss2 3505 . . . . . . . . . . . . . . . . . 18  |-  ( J  i^i  ~P ( `' F " x ) )  C_  ~P ( `' F " x )
52 simprl 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  w  e.  ( J  i^i  ~P ( `' F " x ) ) )
5351, 52sseldi 3289 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  w  e.  ~P ( `' F " x ) )
5453elpwid 3751 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  w  C_  ( `' F " x ) )
55 funimass2 5467 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  F  /\  w  C_  ( `' F "
x ) )  -> 
( F " w
)  C_  x )
5650, 54, 55syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( F "
w )  C_  x
)
575ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  x  C_  Y
)
5856, 57sstrd 3301 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( F "
w )  C_  Y
)
59 f1of1 5613 . . . . . . . . . . . . . . . . 17  |-  ( F : X -1-1-onto-> Y  ->  F : X -1-1-> Y )
6048, 59syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  F : X -1-1-> Y )
61 inss1 3504 . . . . . . . . . . . . . . . . . 18  |-  ( J  i^i  ~P ( `' F " x ) )  C_  J
6261, 52sseldi 3289 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  w  e.  J
)
63 elssuni 3985 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  J  ->  w  C_ 
U. J )
6463, 19syl6sseqr 3338 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  J  ->  w  C_  X )
6562, 64syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  w  C_  X
)
66 f1imacnv 5631 . . . . . . . . . . . . . . . 16  |-  ( ( F : X -1-1-> Y  /\  w  C_  X )  ->  ( `' F " ( F " w
) )  =  w )
6760, 65, 66syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( `' F " ( F " w
) )  =  w )
6867, 62eqeltrd 2461 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( `' F " ( F " w
) )  e.  J
)
6919elqtop2 17654 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  TopBases  /\  F : X -onto-> Y )  ->  (
( F " w
)  e.  ( J qTop 
F )  <->  ( ( F " w )  C_  Y  /\  ( `' F " ( F " w
) )  e.  J
) ) )
707, 69sylan2 461 . . . . . . . . . . . . . . 15  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
( F " w
)  e.  ( J qTop 
F )  <->  ( ( F " w )  C_  Y  /\  ( `' F " ( F " w
) )  e.  J
) ) )
7170ad3antrrr 711 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( ( F
" w )  e.  ( J qTop  F )  <-> 
( ( F "
w )  C_  Y  /\  ( `' F "
( F " w
) )  e.  J
) ) )
7258, 68, 71mpbir2and 889 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( F "
w )  e.  ( J qTop  F ) )
73 vex 2902 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
7473elpw2 4305 . . . . . . . . . . . . . 14  |-  ( ( F " w )  e.  ~P x  <->  ( F " w )  C_  x
)
7556, 74sylibr 204 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( F "
w )  e.  ~P x )
76 elin 3473 . . . . . . . . . . . . 13  |-  ( ( F " w )  e.  ( ( J qTop 
F )  i^i  ~P x )  <->  ( ( F " w )  e.  ( J qTop  F )  /\  ( F "
w )  e.  ~P x ) )
7772, 75, 76sylanbrc 646 . . . . . . . . . . . 12  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( F "
w )  e.  ( ( J qTop  F )  i^i  ~P x ) )
785sselda 3291 . . . . . . . . . . . . . . 15  |-  ( ( ( ( J  e.  TopBases 
/\  F : X -1-1-onto-> Y
)  /\  x  C_  Y
)  /\  y  e.  x )  ->  y  e.  Y )
7978adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  y  e.  Y
)
80 f1ocnvfv2 5954 . . . . . . . . . . . . . 14  |-  ( ( F : X -1-1-onto-> Y  /\  y  e.  Y )  ->  ( F `  ( `' F `  y ) )  =  y )
8148, 79, 80syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( F `  ( `' F `  y ) )  =  y )
82 f1ofn 5615 . . . . . . . . . . . . . . . 16  |-  ( F : X -1-1-onto-> Y  ->  F  Fn  X )
8382adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  F  Fn  X )
8483ad3antrrr 711 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  F  Fn  X
)
85 simprr 734 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( `' F `  y )  e.  w
)
86 fnfvima 5915 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  X  /\  w  C_  X  /\  ( `' F `  y )  e.  w )  -> 
( F `  ( `' F `  y ) )  e.  ( F
" w ) )
8784, 65, 85, 86syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  ( F `  ( `' F `  y ) )  e.  ( F
" w ) )
8881, 87eqeltrrd 2462 . . . . . . . . . . . 12  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  y  e.  ( F " w ) )
89 eleq2 2448 . . . . . . . . . . . . 13  |-  ( z  =  ( F "
w )  ->  (
y  e.  z  <->  y  e.  ( F " w ) ) )
9089rspcev 2995 . . . . . . . . . . . 12  |-  ( ( ( F " w
)  e.  ( ( J qTop  F )  i^i 
~P x )  /\  y  e.  ( F " w ) )  ->  E. z  e.  (
( J qTop  F )  i^i  ~P x ) y  e.  z )
9177, 88, 90syl2anc 643 . . . . . . . . . . 11  |-  ( ( ( ( ( J  e.  TopBases  /\  F : X
-1-1-onto-> Y )  /\  x  C_  Y )  /\  y  e.  x )  /\  (
w  e.  ( J  i^i  ~P ( `' F " x ) )  /\  ( `' F `  y )  e.  w ) )  ->  E. z  e.  ( ( J qTop  F )  i^i  ~P x ) y  e.  z )
9291rexlimdvaa 2774 . . . . . . . . . 10  |-  ( ( ( ( J  e.  TopBases 
/\  F : X -1-1-onto-> Y
)  /\  x  C_  Y
)  /\  y  e.  x )  ->  ( E. w  e.  ( J  i^i  ~P ( `' F " x ) ) ( `' F `  y )  e.  w  ->  E. z  e.  ( ( J qTop  F )  i^i  ~P x ) y  e.  z ) )
9347, 92impbid 184 . . . . . . . . 9  |-  ( ( ( ( J  e.  TopBases 
/\  F : X -1-1-onto-> Y
)  /\  x  C_  Y
)  /\  y  e.  x )  ->  ( E. z  e.  (
( J qTop  F )  i^i  ~P x ) y  e.  z  <->  E. w  e.  ( J  i^i  ~P ( `' F " x ) ) ( `' F `  y )  e.  w
) )
94 eluni2 3961 . . . . . . . . 9  |-  ( y  e.  U. ( ( J qTop  F )  i^i 
~P x )  <->  E. z  e.  ( ( J qTop  F
)  i^i  ~P x
) y  e.  z )
95 eluni2 3961 . . . . . . . . 9  |-  ( ( `' F `  y )  e.  U. ( J  i^i  ~P ( `' F " x ) )  <->  E. w  e.  ( J  i^i  ~P ( `' F " x ) ) ( `' F `  y )  e.  w
)
9693, 94, 953bitr4g 280 . . . . . . . 8  |-  ( ( ( ( J  e.  TopBases 
/\  F : X -1-1-onto-> Y
)  /\  x  C_  Y
)  /\  y  e.  x )  ->  (
y  e.  U. (
( J qTop  F )  i^i  ~P x )  <->  ( `' F `  y )  e.  U. ( J  i^i  ~P ( `' F "
x ) ) ) )
9796ralbidva 2665 . . . . . . 7  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  ( A. y  e.  x  y  e.  U. (
( J qTop  F )  i^i  ~P x )  <->  A. y  e.  x  ( `' F `  y )  e.  U. ( J  i^i  ~P ( `' F "
x ) ) ) )
9815, 97syl5bb 249 . . . . . 6  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  (
x  C_  U. (
( J qTop  F )  i^i  ~P x )  <->  A. y  e.  x  ( `' F `  y )  e.  U. ( J  i^i  ~P ( `' F "
x ) ) ) )
9914, 98bitr4d 248 . . . . 5  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  (
( `' F "
x )  C_  U. ( J  i^i  ~P ( `' F " x ) )  <->  x  C_  U. (
( J qTop  F )  i^i  ~P x ) ) )
100 eltg 16945 . . . . . 6  |-  ( J  e.  TopBases  ->  ( ( `' F " x )  e.  ( topGen `  J
)  <->  ( `' F " x )  C_  U. ( J  i^i  ~P ( `' F " x ) ) ) )
101100ad2antrr 707 . . . . 5  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  (
( `' F "
x )  e.  (
topGen `  J )  <->  ( `' F " x )  C_  U. ( J  i^i  ~P ( `' F " x ) ) ) )
102 ovex 6045 . . . . . 6  |-  ( J qTop 
F )  e.  _V
103 eltg 16945 . . . . . 6  |-  ( ( J qTop  F )  e. 
_V  ->  ( x  e.  ( topGen `  ( J qTop  F ) )  <->  x  C_  U. (
( J qTop  F )  i^i  ~P x ) ) )
104102, 103mp1i 12 . . . . 5  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  (
x  e.  ( topGen `  ( J qTop  F ) )  <->  x  C_  U. (
( J qTop  F )  i^i  ~P x ) ) )
10599, 101, 1043bitr4d 277 . . . 4  |-  ( ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  /\  x  C_  Y )  ->  (
( `' F "
x )  e.  (
topGen `  J )  <->  x  e.  ( topGen `  ( J qTop  F ) ) ) )
106105pm5.32da 623 . . 3  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
( x  C_  Y  /\  ( `' F "
x )  e.  (
topGen `  J ) )  <-> 
( x  C_  Y  /\  x  e.  ( topGen `
 ( J qTop  F
) ) ) ) )
107 tgtopon 16959 . . . . . 6  |-  ( J  e.  TopBases  ->  ( topGen `  J
)  e.  (TopOn `  U. J ) )
108107adantr 452 . . . . 5  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  ( topGen `
 J )  e.  (TopOn `  U. J ) )
10919fveq2i 5671 . . . . 5  |-  (TopOn `  X )  =  (TopOn `  U. J )
110108, 109syl6eleqr 2478 . . . 4  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  ( topGen `
 J )  e.  (TopOn `  X )
)
1117adantl 453 . . . 4  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  F : X -onto-> Y )
112 elqtop3 17656 . . . 4  |-  ( ( ( topGen `  J )  e.  (TopOn `  X )  /\  F : X -onto-> Y
)  ->  ( x  e.  ( ( topGen `  J
) qTop  F )  <->  ( x  C_  Y  /\  ( `' F " x )  e.  ( topGen `  J
) ) ) )
113110, 111, 112syl2anc 643 . . 3  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
x  e.  ( (
topGen `  J ) qTop  F
)  <->  ( x  C_  Y  /\  ( `' F " x )  e.  (
topGen `  J ) ) ) )
114 unitg 16955 . . . . . . . . 9  |-  ( ( J qTop  F )  e. 
_V  ->  U. ( topGen `  ( J qTop  F ) )  = 
U. ( J qTop  F
) )
115102, 114ax-mp 8 . . . . . . . 8  |-  U. ( topGen `
 ( J qTop  F
) )  =  U. ( J qTop  F )
11619elqtop2 17654 . . . . . . . . . . . 12  |-  ( ( J  e.  TopBases  /\  F : X -onto-> Y )  ->  (
x  e.  ( J qTop 
F )  <->  ( x  C_  Y  /\  ( `' F " x )  e.  J ) ) )
1177, 116sylan2 461 . . . . . . . . . . 11  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
x  e.  ( J qTop 
F )  <->  ( x  C_  Y  /\  ( `' F " x )  e.  J ) ) )
118 simpl 444 . . . . . . . . . . . 12  |-  ( ( x  C_  Y  /\  ( `' F " x )  e.  J )  ->  x  C_  Y )
11973elpw 3748 . . . . . . . . . . . 12  |-  ( x  e.  ~P Y  <->  x  C_  Y
)
120118, 119sylibr 204 . . . . . . . . . . 11  |-  ( ( x  C_  Y  /\  ( `' F " x )  e.  J )  ->  x  e.  ~P Y
)
121117, 120syl6bi 220 . . . . . . . . . 10  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
x  e.  ( J qTop 
F )  ->  x  e.  ~P Y ) )
122121ssrdv 3297 . . . . . . . . 9  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  ( J qTop  F )  C_  ~P Y )
123 sspwuni 4117 . . . . . . . . 9  |-  ( ( J qTop  F )  C_  ~P Y  <->  U. ( J qTop  F
)  C_  Y )
124122, 123sylib 189 . . . . . . . 8  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  U. ( J qTop  F )  C_  Y
)
125115, 124syl5eqss 3335 . . . . . . 7  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  U. ( topGen `
 ( J qTop  F
) )  C_  Y
)
126 sspwuni 4117 . . . . . . 7  |-  ( (
topGen `  ( J qTop  F
) )  C_  ~P Y 
<-> 
U. ( topGen `  ( J qTop  F ) )  C_  Y )
127125, 126sylibr 204 . . . . . 6  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  ( topGen `
 ( J qTop  F
) )  C_  ~P Y )
128127sseld 3290 . . . . 5  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
x  e.  ( topGen `  ( J qTop  F ) )  ->  x  e.  ~P Y ) )
129 elpwi 3750 . . . . 5  |-  ( x  e.  ~P Y  ->  x  C_  Y )
130128, 129syl6 31 . . . 4  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
x  e.  ( topGen `  ( J qTop  F ) )  ->  x  C_  Y
) )
131130pm4.71rd 617 . . 3  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
x  e.  ( topGen `  ( J qTop  F ) )  <->  ( x  C_  Y  /\  x  e.  (
topGen `  ( J qTop  F
) ) ) ) )
132106, 113, 1313bitr4d 277 . 2  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
x  e.  ( (
topGen `  J ) qTop  F
)  <->  x  e.  ( topGen `
 ( J qTop  F
) ) ) )
133132eqrdv 2385 1  |-  ( ( J  e.  TopBases  /\  F : X -1-1-onto-> Y )  ->  (
( topGen `  J ) qTop  F )  =  ( topGen `  ( J qTop  F ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2649   E.wrex 2650   _Vcvv 2899    i^i cin 3262    C_ wss 3263   ~Pcpw 3742   U.cuni 3957   `'ccnv 4817   dom cdm 4818   ran crn 4819   "cima 4821   Fun wfun 5388    Fn wfn 5389   -1-1->wf1 5391   -onto->wfo 5392   -1-1-onto->wf1o 5393   ` cfv 5394  (class class class)co 6020   topGenctg 13592   qTop cqtop 13656  TopOnctopon 16882   TopBasesctb 16885
This theorem is referenced by:  imasf1oxms  18409
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 2368  ax-rep 4261  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641
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 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-reu 2656  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-topgen 13594  df-qtop 13660  df-top 16886  df-bases 16888  df-topon 16889
  Copyright terms: Public domain W3C validator