Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  qtophaus Structured version   Unicode version

Theorem qtophaus 27664
Description: If an open map's graph in the product space  ( J  tX  J ) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.)
Hypotheses
Ref Expression
qtophaus.x  |-  X  = 
U. J
qtophaus.e  |-  .~  =  ( `' F  o.  F
)
qtophaus.h  |-  H  =  ( x  e.  X ,  y  e.  X  |-> 
<. ( F `  x
) ,  ( F `
 y ) >.
)
qtophaus.1  |-  ( ph  ->  J  e.  Haus )
qtophaus.2  |-  ( ph  ->  F : X -onto-> Y
)
qtophaus.3  |-  ( (
ph  /\  x  e.  J )  ->  ( F " x )  e.  ( J qTop  F ) )
qtophaus.4  |-  ( ph  ->  .~  e.  ( Clsd `  ( J  tX  J
) ) )
Assertion
Ref Expression
qtophaus  |-  ( ph  ->  ( J qTop  F )  e.  Haus )
Distinct variable groups:    x,  .~ , y    x, F, y    x, H, y    x, J, y   
x, X, y    x, Y, y    ph, x, y

Proof of Theorem qtophaus
Dummy variables  a 
b  c  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qtophaus.1 . . . . 5  |-  ( ph  ->  J  e.  Haus )
2 haustop 19700 . . . . 5  |-  ( J  e.  Haus  ->  J  e. 
Top )
31, 2syl 16 . . . 4  |-  ( ph  ->  J  e.  Top )
4 qtophaus.2 . . . . 5  |-  ( ph  ->  F : X -onto-> Y
)
5 fofn 5803 . . . . 5  |-  ( F : X -onto-> Y  ->  F  Fn  X )
64, 5syl 16 . . . 4  |-  ( ph  ->  F  Fn  X )
7 qtophaus.x . . . . 5  |-  X  = 
U. J
87qtoptop 20069 . . . 4  |-  ( ( J  e.  Top  /\  F  Fn  X )  ->  ( J qTop  F )  e.  Top )
93, 6, 8syl2anc 661 . . 3  |-  ( ph  ->  ( J qTop  F )  e.  Top )
10 txtop 19938 . . . . 5  |-  ( ( ( J qTop  F )  e.  Top  /\  ( J qTop  F )  e.  Top )  ->  ( ( J qTop 
F )  tX  ( J qTop  F ) )  e. 
Top )
119, 9, 10syl2anc 661 . . . 4  |-  ( ph  ->  ( ( J qTop  F
)  tX  ( J qTop  F ) )  e.  Top )
12 idssxp 27292 . . . . . 6  |-  (  _I  |`  U. ( J qTop  F
) )  C_  ( U. ( J qTop  F )  X.  U. ( J qTop 
F ) )
1312a1i 11 . . . . 5  |-  ( ph  ->  (  _I  |`  U. ( J qTop  F ) )  C_  ( U. ( J qTop  F
)  X.  U. ( J qTop  F ) ) )
14 eqid 2467 . . . . . . 7  |-  U. ( J qTop  F )  =  U. ( J qTop  F )
1514, 14txuni 19961 . . . . . 6  |-  ( ( ( J qTop  F )  e.  Top  /\  ( J qTop  F )  e.  Top )  ->  ( U. ( J qTop  F )  X.  U. ( J qTop  F )
)  =  U. (
( J qTop  F )  tX  ( J qTop  F ) ) )
169, 9, 15syl2anc 661 . . . . 5  |-  ( ph  ->  ( U. ( J qTop 
F )  X.  U. ( J qTop  F )
)  =  U. (
( J qTop  F )  tX  ( J qTop  F ) ) )
1713, 16sseqtrd 3545 . . . 4  |-  ( ph  ->  (  _I  |`  U. ( J qTop  F ) )  C_  U. ( ( J qTop  F
)  tX  ( J qTop  F ) ) )
187qtopuni 20071 . . . . . . . . 9  |-  ( ( J  e.  Top  /\  F : X -onto-> Y )  ->  Y  =  U. ( J qTop  F )
)
193, 4, 18syl2anc 661 . . . . . . . 8  |-  ( ph  ->  Y  =  U. ( J qTop  F ) )
2019, 19xpeq12d 5030 . . . . . . 7  |-  ( ph  ->  ( Y  X.  Y
)  =  ( U. ( J qTop  F )  X.  U. ( J qTop  F
) ) )
2120, 16eqtr2d 2509 . . . . . 6  |-  ( ph  ->  U. ( ( J qTop 
F )  tX  ( J qTop  F ) )  =  ( Y  X.  Y
) )
2219eqcomd 2475 . . . . . . 7  |-  ( ph  ->  U. ( J qTop  F
)  =  Y )
2322reseq2d 5279 . . . . . 6  |-  ( ph  ->  (  _I  |`  U. ( J qTop  F ) )  =  (  _I  |`  Y ) )
2421, 23difeq12d 3628 . . . . 5  |-  ( ph  ->  ( U. ( ( J qTop  F )  tX  ( J qTop  F )
)  \  (  _I  |` 
U. ( J qTop  F
) ) )  =  ( ( Y  X.  Y )  \  (  _I  |`  Y ) ) )
25 simp-4r 766 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  x  e.  X
)
26 simplr 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  y  e.  X
)
27 opelxpi 5037 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  X  /\  y  e.  X )  -> 
<. x ,  y >.  e.  ( X  X.  X
) )
2825, 26, 27syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  <. x ,  y
>.  e.  ( X  X.  X ) )
29 df-br 4454 . . . . . . . . . . . . . . . . 17  |-  ( x ( X  X.  X
) y  <->  <. x ,  y >.  e.  ( X  X.  X ) )
3028, 29sylibr 212 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  x ( X  X.  X ) y )
31 simpllr 758 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  ( F `  x )  =  a )
32 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  ( F `  y )  =  b )
3331, 32opeq12d 4227 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  <. ( F `  x ) ,  ( F `  y )
>.  =  <. a ,  b >. )
34 simp-5r 768 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  c  =  <. a ,  b >. )
35 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  ->  c  e.  ( ( Y  X.  Y )  \  _I  ) )
3635ad7antr 737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  c  e.  ( ( Y  X.  Y
)  \  _I  )
)
3734, 36eqeltrrd 2556 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  <. a ,  b
>.  e.  ( ( Y  X.  Y )  \  _I  ) )
3833, 37eqeltrd 2555 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  <. ( F `  x ) ,  ( F `  y )
>.  e.  ( ( Y  X.  Y )  \  _I  ) )
39 relxp 5116 . . . . . . . . . . . . . . . . . . . 20  |-  Rel  ( Y  X.  Y )
40 opeldifid 27279 . . . . . . . . . . . . . . . . . . . 20  |-  ( Rel  ( Y  X.  Y
)  ->  ( <. ( F `  x ) ,  ( F `  y ) >.  e.  ( ( Y  X.  Y
)  \  _I  )  <->  (
<. ( F `  x
) ,  ( F `
 y ) >.  e.  ( Y  X.  Y
)  /\  ( F `  x )  =/=  ( F `  y )
) ) )
4139, 40ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( <.
( F `  x
) ,  ( F `
 y ) >.  e.  ( ( Y  X.  Y )  \  _I  ) 
<->  ( <. ( F `  x ) ,  ( F `  y )
>.  e.  ( Y  X.  Y )  /\  ( F `  x )  =/=  ( F `  y
) ) )
4238, 41sylib 196 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  ( <. ( F `  x ) ,  ( F `  y ) >.  e.  ( Y  X.  Y )  /\  ( F `  x )  =/=  ( F `  y )
) )
4342simprd 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  ( F `  x )  =/=  ( F `  y )
)
446ad8antr 739 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  F  Fn  X
)
45 qtophaus.e . . . . . . . . . . . . . . . . . . . 20  |-  .~  =  ( `' F  o.  F
)
4645fcoinvbr 27284 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F  Fn  X  /\  x  e.  X  /\  y  e.  X )  ->  ( x  .~  y  <->  ( F `  x )  =  ( F `  y ) ) )
4744, 25, 26, 46syl3anc 1228 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  ( x  .~  y 
<->  ( F `  x
)  =  ( F `
 y ) ) )
4847necon3bbid 2714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  ( -.  x  .~  y  <->  ( F `  x )  =/=  ( F `  y )
) )
4943, 48mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  -.  x  .~  y )
5030, 49jca 532 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  ( x ( X  X.  X ) y  /\  -.  x  .~  y ) )
51 df-br 4454 . . . . . . . . . . . . . . . 16  |-  ( x ( ( X  X.  X )  \  .~  ) y  <->  <. x ,  y >.  e.  (
( X  X.  X
)  \  .~  )
)
52 brdif 4503 . . . . . . . . . . . . . . . 16  |-  ( x ( ( X  X.  X )  \  .~  ) y  <->  ( x
( X  X.  X
) y  /\  -.  x  .~  y ) )
5351, 52bitr3i 251 . . . . . . . . . . . . . . 15  |-  ( <.
x ,  y >.  e.  ( ( X  X.  X )  \  .~  ) 
<->  ( x ( X  X.  X ) y  /\  -.  x  .~  y ) )
5450, 53sylibr 212 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  <. x ,  y
>.  e.  ( ( X  X.  X )  \  .~  ) )
55 qtophaus.h . . . . . . . . . . . . . . . 16  |-  H  =  ( x  e.  X ,  y  e.  X  |-> 
<. ( F `  x
) ,  ( F `
 y ) >.
)
5655, 25, 26fvproj 27660 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  ( H `  <. x ,  y >.
)  =  <. ( F `  x ) ,  ( F `  y ) >. )
5733, 56, 343eqtr4d 2518 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  ( H `  <. x ,  y >.
)  =  c )
58 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( z  =  <. x ,  y
>.  ->  ( H `  z )  =  ( H `  <. x ,  y >. )
)
59 eqidd 2468 . . . . . . . . . . . . . . . 16  |-  ( z  =  <. x ,  y
>.  ->  c  =  c )
6058, 59eqeq12d 2489 . . . . . . . . . . . . . . 15  |-  ( z  =  <. x ,  y
>.  ->  ( ( H `
 z )  =  c  <->  ( H `  <. x ,  y >.
)  =  c ) )
6160rspcev 3219 . . . . . . . . . . . . . 14  |-  ( (
<. x ,  y >.  e.  ( ( X  X.  X )  \  .~  )  /\  ( H `  <. x ,  y >.
)  =  c )  ->  E. z  e.  ( ( X  X.  X
)  \  .~  )
( H `  z
)  =  c )
6254, 57, 61syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  /\  y  e.  X )  /\  ( F `  y
)  =  b )  ->  E. z  e.  ( ( X  X.  X
)  \  .~  )
( H `  z
)  =  c )
63 fofun 5802 . . . . . . . . . . . . . . . . 17  |-  ( F : X -onto-> Y  ->  Fun  F )
644, 63syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Fun  F )
6564ad4antr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  ->  Fun  F
)
6665ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  /\  a  e.  Y )  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  ->  Fun  F )
67 simp-4r 766 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  /\  a  e.  Y )  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  -> 
b  e.  Y )
68 foima 5806 . . . . . . . . . . . . . . . . . 18  |-  ( F : X -onto-> Y  -> 
( F " X
)  =  Y )
694, 68syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F " X
)  =  Y )
7069ad4antr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  ->  ( F
" X )  =  Y )
7170ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  /\  a  e.  Y )  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  -> 
( F " X
)  =  Y )
7267, 71eleqtrrd 2558 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  /\  a  e.  Y )  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  -> 
b  e.  ( F
" X ) )
73 fvelima 5926 . . . . . . . . . . . . . 14  |-  ( ( Fun  F  /\  b  e.  ( F " X
) )  ->  E. y  e.  X  ( F `  y )  =  b )
7466, 72, 73syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  /\  a  e.  Y )  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  ->  E. y  e.  X  ( F `  y )  =  b )
7562, 74r19.29a 3008 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  /\  a  e.  Y )  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  /\  x  e.  X )  /\  ( F `  x )  =  a )  ->  E. z  e.  (
( X  X.  X
)  \  .~  )
( H `  z
)  =  c )
76 simpllr 758 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  ->  a  e.  Y )
7776, 70eleqtrrd 2558 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  ->  a  e.  ( F " X
) )
78 fvelima 5926 . . . . . . . . . . . . 13  |-  ( ( Fun  F  /\  a  e.  ( F " X
) )  ->  E. x  e.  X  ( F `  x )  =  a )
7965, 77, 78syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  ->  E. x  e.  X  ( F `  x )  =  a )
8075, 79r19.29a 3008 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  c  e.  ( ( Y  X.  Y ) 
\  _I  ) )  /\  a  e.  Y
)  /\  b  e.  Y )  /\  c  =  <. a ,  b
>. )  ->  E. z  e.  ( ( X  X.  X )  \  .~  ) ( H `  z )  =  c )
8135eldifad 3493 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  ->  c  e.  ( Y  X.  Y
) )
82 elxp2 5023 . . . . . . . . . . . 12  |-  ( c  e.  ( Y  X.  Y )  <->  E. a  e.  Y  E. b  e.  Y  c  =  <. a ,  b >.
)
8381, 82sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  ->  E. a  e.  Y  E. b  e.  Y  c  =  <. a ,  b >.
)
8480, 83r19.29_2a 3010 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  ( ( Y  X.  Y )  \  _I  ) )  ->  E. z  e.  ( ( X  X.  X )  \  .~  ) ( H `  z )  =  c )
85 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  z  =  <. x ,  y >.
)
8685fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( H `  z )  =  ( H `  <. x ,  y >. )
)
87 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  -> 
( H `  z
)  =  c )
8887ad3antrrr 729 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( H `  z )  =  c )
89 simpllr 758 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  z  e.  ( ( X  X.  X ) 
\  .~  ) )  /\  x  e.  X
)  /\  y  e.  X )  /\  z  =  <. x ,  y
>. )  ->  x  e.  X )
9089adantl3r 749 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  x  e.  X )
91 simplr 754 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  z  e.  ( ( X  X.  X ) 
\  .~  ) )  /\  x  e.  X
)  /\  y  e.  X )  /\  z  =  <. x ,  y
>. )  ->  y  e.  X )
9291adantl3r 749 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  y  e.  X )
9355, 90, 92fvproj 27660 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( H `  <. x ,  y
>. )  =  <. ( F `  x ) ,  ( F `  y ) >. )
9486, 88, 933eqtr3d 2516 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  c  =  <. ( F `  x
) ,  ( F `
 y ) >.
)
95 fof 5801 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : X -onto-> Y  ->  F : X --> Y )
964, 95syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F : X --> Y )
9796ad5antr 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  F : X
--> Y )
9897, 90ffvelrnd 6033 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( F `  x )  e.  Y
)
9997, 92ffvelrnd 6033 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( F `  y )  e.  Y
)
10098, 99jca 532 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( ( F `  x )  e.  Y  /\  ( F `  y )  e.  Y ) )
101 opelxp 5035 . . . . . . . . . . . . . . . 16  |-  ( <.
( F `  x
) ,  ( F `
 y ) >.  e.  ( Y  X.  Y
)  <->  ( ( F `
 x )  e.  Y  /\  ( F `
 y )  e.  Y ) )
102100, 101sylibr 212 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  <. ( F `
 x ) ,  ( F `  y
) >.  e.  ( Y  X.  Y ) )
103 simp-5r 768 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  z  e.  ( ( X  X.  X )  \  .~  ) )
10485, 103eqeltrrd 2556 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  <. x ,  y >.  e.  (
( X  X.  X
)  \  .~  )
)
10553simprbi 464 . . . . . . . . . . . . . . . . 17  |-  ( <.
x ,  y >.  e.  ( ( X  X.  X )  \  .~  )  ->  -.  x  .~  y )
106104, 105syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  -.  x  .~  y )
1076ad5antr 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  F  Fn  X )
108107, 90, 92, 46syl3anc 1228 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( x  .~  y  <->  ( F `  x )  =  ( F `  y ) ) )
109108necon3bbid 2714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( -.  x  .~  y  <->  ( F `  x )  =/=  ( F `  y )
) )
110106, 109mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( F `  x )  =/=  ( F `  y )
)
111102, 110jca 532 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  ( <. ( F `  x ) ,  ( F `  y ) >.  e.  ( Y  X.  Y )  /\  ( F `  x )  =/=  ( F `  y )
) )
112111, 41sylibr 212 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  <. ( F `
 x ) ,  ( F `  y
) >.  e.  ( ( Y  X.  Y ) 
\  _I  ) )
11394, 112eqeltrd 2555 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  /\  x  e.  X )  /\  y  e.  X
)  /\  z  =  <. x ,  y >.
)  ->  c  e.  ( ( Y  X.  Y )  \  _I  ) )
114 difss 3636 . . . . . . . . . . . . . . . 16  |-  ( ( X  X.  X ) 
\  .~  )  C_  ( X  X.  X
)
115114sseli 3505 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( ( X  X.  X )  \  .~  )  ->  z  e.  ( X  X.  X
) )
116115adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  ->  z  e.  ( X  X.  X
) )
117 elxp2 5023 . . . . . . . . . . . . . 14  |-  ( z  e.  ( X  X.  X )  <->  E. x  e.  X  E. y  e.  X  z  =  <. x ,  y >.
)
118116, 117sylib 196 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  ->  E. x  e.  X  E. y  e.  X  z  =  <. x ,  y >.
)
119118adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  ->  E. x  e.  X  E. y  e.  X  z  =  <. x ,  y >. )
120113, 119r19.29_2a 3010 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  ( ( X  X.  X )  \  .~  ) )  /\  ( H `  z )  =  c )  -> 
c  e.  ( ( Y  X.  Y ) 
\  _I  ) )
121120r19.29an 3007 . . . . . . . . . 10  |-  ( (
ph  /\  E. z  e.  ( ( X  X.  X )  \  .~  ) ( H `  z )  =  c )  ->  c  e.  ( ( Y  X.  Y )  \  _I  ) )
12284, 121impbida 830 . . . . . . . . 9  |-  ( ph  ->  ( c  e.  ( ( Y  X.  Y
)  \  _I  )  <->  E. z  e.  ( ( X  X.  X ) 
\  .~  ) ( H `  z )  =  c ) )
123 opex 4717 . . . . . . . . . . 11  |-  <. ( F `  x ) ,  ( F `  y ) >.  e.  _V
12455, 123fnmpt2i 6864 . . . . . . . . . 10  |-  H  Fn  ( X  X.  X
)
125 fvelimab 5930 . . . . . . . . . 10  |-  ( ( H  Fn  ( X  X.  X )  /\  ( ( X  X.  X )  \  .~  )  C_  ( X  X.  X ) )  -> 
( c  e.  ( H " ( ( X  X.  X ) 
\  .~  ) )  <->  E. z  e.  ( ( X  X.  X ) 
\  .~  ) ( H `  z )  =  c ) )
126124, 114, 125mp2an 672 . . . . . . . . 9  |-  ( c  e.  ( H "
( ( X  X.  X )  \  .~  ) )  <->  E. z  e.  ( ( X  X.  X )  \  .~  ) ( H `  z )  =  c )
127122, 126syl6rbbr 264 . . . . . . . 8  |-  ( ph  ->  ( c  e.  ( H " ( ( X  X.  X ) 
\  .~  ) )  <->  c  e.  ( ( Y  X.  Y )  \  _I  ) ) )
128127eqrdv 2464 . . . . . . 7  |-  ( ph  ->  ( H " (
( X  X.  X
)  \  .~  )
)  =  ( ( Y  X.  Y ) 
\  _I  ) )
129 ssv 3529 . . . . . . . 8  |-  Y  C_  _V
130 xpss2 5118 . . . . . . . 8  |-  ( Y 
C_  _V  ->  ( Y  X.  Y )  C_  ( Y  X.  _V )
)
131 difres 27280 . . . . . . . 8  |-  ( ( Y  X.  Y ) 
C_  ( Y  X.  _V )  ->  ( ( Y  X.  Y ) 
\  (  _I  |`  Y ) )  =  ( ( Y  X.  Y ) 
\  _I  ) )
132129, 130, 131mp2b 10 . . . . . . 7  |-  ( ( Y  X.  Y ) 
\  (  _I  |`  Y ) )  =  ( ( Y  X.  Y ) 
\  _I  )
133128, 132syl6eqr 2526 . . . . . 6  |-  ( ph  ->  ( H " (
( X  X.  X
)  \  .~  )
)  =  ( ( Y  X.  Y ) 
\  (  _I  |`  Y ) ) )
1347toptopon 19303 . . . . . . . 8  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
1353, 134sylib 196 . . . . . . 7  |-  ( ph  ->  J  e.  (TopOn `  X ) )
136 qtoptopon 20073 . . . . . . . 8  |-  ( ( J  e.  (TopOn `  X )  /\  F : X -onto-> Y )  ->  ( J qTop  F )  e.  (TopOn `  Y ) )
137135, 4, 136syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( J qTop  F )  e.  (TopOn `  Y
) )
138 qtophaus.3 . . . . . . 7  |-  ( (
ph  /\  x  e.  J )  ->  ( F " x )  e.  ( J qTop  F ) )
139138ralrimiva 2881 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  J  ( F " x )  e.  ( J qTop  F
) )
140 imaeq2 5339 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( F " x )  =  ( F " y
) )
141 eqidd 2468 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( J qTop  F )  =  ( J qTop  F ) )
142140, 141eleq12d 2549 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( F " x
)  e.  ( J qTop 
F )  <->  ( F " y )  e.  ( J qTop  F ) ) )
143142cbvralv 3093 . . . . . . . . 9  |-  ( A. x  e.  J  ( F " x )  e.  ( J qTop  F )  <->  A. y  e.  J  ( F " y )  e.  ( J qTop  F
) )
144139, 143sylib 196 . . . . . . . 8  |-  ( ph  ->  A. y  e.  J  ( F " y )  e.  ( J qTop  F
) )
145144r19.21bi 2836 . . . . . . 7  |-  ( (
ph  /\  y  e.  J )  ->  ( F " y )  e.  ( J qTop  F ) )
1463, 3jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( J  e.  Top  /\  J  e.  Top )
)
1477, 7txuni 19961 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  J  e.  Top )  ->  ( X  X.  X
)  =  U. ( J  tX  J ) )
148146, 147syl 16 . . . . . . . . 9  |-  ( ph  ->  ( X  X.  X
)  =  U. ( J  tX  J ) )
149148difeq1d 3626 . . . . . . . 8  |-  ( ph  ->  ( ( X  X.  X )  \  .~  )  =  ( U. ( J  tX  J ) 
\  .~  ) )
150 qtophaus.4 . . . . . . . . 9  |-  ( ph  ->  .~  e.  ( Clsd `  ( J  tX  J
) ) )
151 txtop 19938 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  J  e.  Top )  ->  ( J  tX  J
)  e.  Top )
152146, 151syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( J  tX  J
)  e.  Top )
153 fcoinver 27283 . . . . . . . . . . . . . 14  |-  ( F  Fn  X  ->  ( `' F  o.  F
)  Er  X )
1546, 153syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' F  o.  F )  Er  X
)
155 ereq1 7330 . . . . . . . . . . . . . 14  |-  (  .~  =  ( `' F  o.  F )  ->  (  .~  Er  X  <->  ( `' F  o.  F )  Er  X ) )
15645, 155ax-mp 5 . . . . . . . . . . . . 13  |-  (  .~  Er  X  <->  ( `' F  o.  F )  Er  X
)
157154, 156sylibr 212 . . . . . . . . . . . 12  |-  ( ph  ->  .~  Er  X )
158 erssxp 7346 . . . . . . . . . . . 12  |-  (  .~  Er  X  ->  .~  C_  ( X  X.  X ) )
159157, 158syl 16 . . . . . . . . . . 11  |-  ( ph  ->  .~  C_  ( X  X.  X ) )
160159, 148sseqtrd 3545 . . . . . . . . . 10  |-  ( ph  ->  .~  C_  U. ( J  tX  J ) )
161 eqid 2467 . . . . . . . . . . 11  |-  U. ( J  tX  J )  = 
U. ( J  tX  J )
162161iscld2 19397 . . . . . . . . . 10  |-  ( ( ( J  tX  J
)  e.  Top  /\  .~  C_  U. ( J  tX  J ) )  -> 
(  .~  e.  ( Clsd `  ( J  tX  J ) )  <->  ( U. ( J  tX  J ) 
\  .~  )  e.  ( J  tX  J ) ) )
163152, 160, 162syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  (  .~  e.  (
Clsd `  ( J  tX  J ) )  <->  ( U. ( J  tX  J ) 
\  .~  )  e.  ( J  tX  J ) ) )
164150, 163mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( U. ( J 
tX  J )  \  .~  )  e.  ( J  tX  J ) )
165149, 164eqeltrd 2555 . . . . . . 7  |-  ( ph  ->  ( ( X  X.  X )  \  .~  )  e.  ( J  tX  J ) )
16696, 96, 135, 135, 137, 137, 138, 145, 165, 55txomap 27662 . . . . . 6  |-  ( ph  ->  ( H " (
( X  X.  X
)  \  .~  )
)  e.  ( ( J qTop  F )  tX  ( J qTop  F )
) )
167133, 166eqeltrrd 2556 . . . . 5  |-  ( ph  ->  ( ( Y  X.  Y )  \  (  _I  |`  Y ) )  e.  ( ( J qTop 
F )  tX  ( J qTop  F ) ) )
16824, 167eqeltrd 2555 . . . 4  |-  ( ph  ->  ( U. ( ( J qTop  F )  tX  ( J qTop  F )
)  \  (  _I  |` 
U. ( J qTop  F
) ) )  e.  ( ( J qTop  F
)  tX  ( J qTop  F ) ) )
169 eqid 2467 . . . . . 6  |-  U. (
( J qTop  F )  tX  ( J qTop  F ) )  =  U. (
( J qTop  F )  tX  ( J qTop  F ) )
170169iscld2 19397 . . . . 5  |-  ( ( ( ( J qTop  F
)  tX  ( J qTop  F ) )  e.  Top  /\  (  _I  |`  U. ( J qTop  F ) )  C_  U. ( ( J qTop  F
)  tX  ( J qTop  F ) ) )  -> 
( (  _I  |`  U. ( J qTop  F ) )  e.  ( Clsd `  (
( J qTop  F )  tX  ( J qTop  F ) ) )  <->  ( U. ( ( J qTop  F
)  tX  ( J qTop  F ) )  \  (  _I  |`  U. ( J qTop 
F ) ) )  e.  ( ( J qTop 
F )  tX  ( J qTop  F ) ) ) )
171170biimpar 485 . . . 4  |-  ( ( ( ( ( J qTop 
F )  tX  ( J qTop  F ) )  e. 
Top  /\  (  _I  |` 
U. ( J qTop  F
) )  C_  U. (
( J qTop  F )  tX  ( J qTop  F ) ) )  /\  ( U. ( ( J qTop  F
)  tX  ( J qTop  F ) )  \  (  _I  |`  U. ( J qTop 
F ) ) )  e.  ( ( J qTop 
F )  tX  ( J qTop  F ) ) )  ->  (  _I  |`  U. ( J qTop  F ) )  e.  ( Clsd `  (
( J qTop  F )  tX  ( J qTop  F ) ) ) )
17211, 17, 168, 171syl21anc 1227 . . 3  |-  ( ph  ->  (  _I  |`  U. ( J qTop  F ) )  e.  ( Clsd `  (
( J qTop  F )  tX  ( J qTop  F ) ) ) )
1739, 172jca 532 . 2  |-  ( ph  ->  ( ( J qTop  F
)  e.  Top  /\  (  _I  |`  U. ( J qTop  F ) )  e.  ( Clsd `  (
( J qTop  F )  tX  ( J qTop  F ) ) ) ) )
17414hausdiag 20014 . 2  |-  ( ( J qTop  F )  e. 
Haus 
<->  ( ( J qTop  F
)  e.  Top  /\  (  _I  |`  U. ( J qTop  F ) )  e.  ( Clsd `  (
( J qTop  F )  tX  ( J qTop  F ) ) ) ) )
175173, 174sylibr 212 1  |-  ( ph  ->  ( J qTop  F )  e.  Haus )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767    =/= wne 2662   A.wral 2817   E.wrex 2818   _Vcvv 3118    \ cdif 3478    C_ wss 3481   <.cop 4039   U.cuni 4251   class class class wbr 4453    _I cid 4796    X. cxp 5003   `'ccnv 5004    |` cres 5007   "cima 5008    o. ccom 5009   Rel wrel 5010   Fun wfun 5588    Fn wfn 5589   -->wf 5590   -onto->wfo 5592   ` cfv 5594  (class class class)co 6295    |-> cmpt2 6297    Er wer 7320   qTop cqtop 14775   Topctop 19263  TopOnctopon 19264   Clsdccld 19385   Hauscha 19677    tX ctx 19929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-1st 6795  df-2nd 6796  df-er 7323  df-topgen 14716  df-qtop 14779  df-top 19268  df-bases 19270  df-topon 19271  df-cld 19388  df-haus 19684  df-tx 19931
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator