Metamath Proof Explorer

Theorem qtophaus

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)

Ref Expression
Hypotheses 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 qtophaus 
|- ( ph -> ( J qTop F ) e. Haus )

Proof

Step Hyp Ref Expression
1 qtophaus.x 
 |-  X = U. J
2 qtophaus.e 
 |-  .~ = ( `' F o. F )
3 qtophaus.h 
 |-  H = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )
4 qtophaus.1 
 |-  ( ph -> J e. Haus )
5 qtophaus.2 
 |-  ( ph -> F : X -onto-> Y )
6 qtophaus.3 
 |-  ( ( ph /\ x e. J ) -> ( F " x ) e. ( J qTop F ) )
7 qtophaus.4 
 |-  ( ph -> .~ e. ( Clsd ` ( J tX J ) ) )
8 haustop 
 |-  ( J e. Haus -> J e. Top )
9 4 8 syl 
 |-  ( ph -> J e. Top )
10 fofn 
 |-  ( F : X -onto-> Y -> F Fn X )
11 5 10 syl 
 |-  ( ph -> F Fn X )
12 1 qtoptop 
 |-  ( ( J e. Top /\ F Fn X ) -> ( J qTop F ) e. Top )
13 9 11 12 syl2anc 
 |-  ( ph -> ( J qTop F ) e. Top )
14 txtop 
 |-  ( ( ( J qTop F ) e. Top /\ ( J qTop F ) e. Top ) -> ( ( J qTop F ) tX ( J qTop F ) ) e. Top )
15 13 13 14 syl2anc 
 |-  ( ph -> ( ( J qTop F ) tX ( J qTop F ) ) e. Top )
16 idssxp 
 |-  ( _I |` U. ( J qTop F ) ) C_ ( U. ( J qTop F ) X. U. ( J qTop F ) )
17 eqid 
 |-  U. ( J qTop F ) = U. ( J qTop F )
18 17 17 txuni 
 |-  ( ( ( 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 ) ) )
19 13 13 18 syl2anc 
 |-  ( ph -> ( U. ( J qTop F ) X. U. ( J qTop F ) ) = U. ( ( J qTop F ) tX ( J qTop F ) ) )
20 16 19 sseqtrid 
 |-  ( ph -> ( _I |` U. ( J qTop F ) ) C_ U. ( ( J qTop F ) tX ( J qTop F ) ) )
21 1 qtopuni 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> Y = U. ( J qTop F ) )
22 9 5 21 syl2anc 
 |-  ( ph -> Y = U. ( J qTop F ) )
23 22 sqxpeqd 
 |-  ( ph -> ( Y X. Y ) = ( U. ( J qTop F ) X. U. ( J qTop F ) ) )
24 23 19 eqtr2d 
 |-  ( ph -> U. ( ( J qTop F ) tX ( J qTop F ) ) = ( Y X. Y ) )
25 22 eqcomd 
 |-  ( ph -> U. ( J qTop F ) = Y )
26 25 reseq2d 
 |-  ( ph -> ( _I |` U. ( J qTop F ) ) = ( _I |` Y ) )
27 24 26 difeq12d 
 |-  ( ph -> ( U. ( ( J qTop F ) tX ( J qTop F ) ) \ ( _I |` U. ( J qTop F ) ) ) = ( ( Y X. Y ) \ ( _I |` Y ) ) )
28 opex 
 |-  <. ( F ` x ) , ( F ` y ) >. e. _V
29 3 28 fnmpoi 
 |-  H Fn ( X X. X )
30 difss 
 |-  ( ( X X. X ) \ .~ ) C_ ( X X. X )
31 fvelimab 
 |-  ( ( 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 ) )
32 29 30 31 mp2an 
 |-  ( c e. ( H " ( ( X X. X ) \ .~ ) ) <-> E. z e. ( ( X X. X ) \ .~ ) ( H ` z ) = c )
33 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( 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 )
34 simplr 
 |-  ( ( ( ( ( ( ( ( ( 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 )
35 opelxpi 
 |-  ( ( x e. X /\ y e. X ) -> <. x , y >. e. ( X X. X ) )
36 33 34 35 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( 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 ) )
37 df-br 
 |-  ( x ( X X. X ) y <-> <. x , y >. e. ( X X. X ) )
38 36 37 sylibr 
 |-  ( ( ( ( ( ( ( ( ( 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 )
39 simpllr 
 |-  ( ( ( ( ( ( ( ( ( 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 )
40 simpr 
 |-  ( ( ( ( ( ( ( ( ( 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 )
41 39 40 opeq12d 
 |-  ( ( ( ( ( ( ( ( ( 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 >. )
42 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( 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 >. )
43 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( 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 ) )
44 42 43 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ( 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 ) )
45 41 44 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( 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 ) )
46 relxp 
 |-  Rel ( Y X. Y )
47 opeldifid 
 |-  ( 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 ) ) ) )
48 46 47 ax-mp 
 |-  ( <. ( F ` x ) , ( F ` y ) >. e. ( ( Y X. Y ) \ _I ) <-> ( <. ( F ` x ) , ( F ` y ) >. e. ( Y X. Y ) /\ ( F ` x ) =/= ( F ` y ) ) )
49 45 48 sylib 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) )
50 49 simprd 
 |-  ( ( ( ( ( ( ( ( ( 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 ) )
51 11 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( 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 )
52 2 fcoinvbr 
 |-  ( ( F Fn X /\ x e. X /\ y e. X ) -> ( x .~ y <-> ( F ` x ) = ( F ` y ) ) )
53 51 33 34 52 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) )
54 53 necon3bbid 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) )
55 50 54 mpbird 
 |-  ( ( ( ( ( ( ( ( ( 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 )
56 df-br 
 |-  ( x ( ( X X. X ) \ .~ ) y <-> <. x , y >. e. ( ( X X. X ) \ .~ ) )
57 brdif 
 |-  ( x ( ( X X. X ) \ .~ ) y <-> ( x ( X X. X ) y /\ -. x .~ y ) )
58 56 57 bitr3i 
 |-  ( <. x , y >. e. ( ( X X. X ) \ .~ ) <-> ( x ( X X. X ) y /\ -. x .~ y ) )
59 38 55 58 sylanbrc 
 |-  ( ( ( ( ( ( ( ( ( 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 ) \ .~ ) )
60 3 33 34 fvproj 
 |-  ( ( ( ( ( ( ( ( ( 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 ) >. )
61 41 60 42 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( 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 )
62 fveqeq2 
 |-  ( z = <. x , y >. -> ( ( H ` z ) = c <-> ( H ` <. x , y >. ) = c ) )
63 62 rspcev 
 |-  ( ( <. x , y >. e. ( ( X X. X ) \ .~ ) /\ ( H ` <. x , y >. ) = c ) -> E. z e. ( ( X X. X ) \ .~ ) ( H ` z ) = c )
64 59 61 63 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( 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 )
65 fofun 
 |-  ( F : X -onto-> Y -> Fun F )
66 5 65 syl 
 |-  ( ph -> Fun F )
67 66 ad4antr 
 |-  ( ( ( ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) /\ a e. Y ) /\ b e. Y ) /\ c = <. a , b >. ) -> Fun F )
68 67 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) /\ a e. Y ) /\ b e. Y ) /\ c = <. a , b >. ) /\ x e. X ) /\ ( F ` x ) = a ) -> Fun F )
69 simp-4r 
 |-  ( ( ( ( ( ( ( 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 )
70 foima 
 |-  ( F : X -onto-> Y -> ( F " X ) = Y )
71 5 70 syl 
 |-  ( ph -> ( F " X ) = Y )
72 71 ad4antr 
 |-  ( ( ( ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) /\ a e. Y ) /\ b e. Y ) /\ c = <. a , b >. ) -> ( F " X ) = Y )
73 72 ad2antrr 
 |-  ( ( ( ( ( ( ( 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 )
74 69 73 eleqtrrd 
 |-  ( ( ( ( ( ( ( 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 ) )
75 fvelima 
 |-  ( ( Fun F /\ b e. ( F " X ) ) -> E. y e. X ( F ` y ) = b )
76 68 74 75 syl2anc 
 |-  ( ( ( ( ( ( ( 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 )
77 64 76 r19.29a 
 |-  ( ( ( ( ( ( ( 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 )
78 simpllr 
 |-  ( ( ( ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) /\ a e. Y ) /\ b e. Y ) /\ c = <. a , b >. ) -> a e. Y )
79 78 72 eleqtrrd 
 |-  ( ( ( ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) /\ a e. Y ) /\ b e. Y ) /\ c = <. a , b >. ) -> a e. ( F " X ) )
80 fvelima 
 |-  ( ( Fun F /\ a e. ( F " X ) ) -> E. x e. X ( F ` x ) = a )
81 67 79 80 syl2anc 
 |-  ( ( ( ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) /\ a e. Y ) /\ b e. Y ) /\ c = <. a , b >. ) -> E. x e. X ( F ` x ) = a )
82 77 81 r19.29a 
 |-  ( ( ( ( ( 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 )
83 simpr 
 |-  ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) -> c e. ( ( Y X. Y ) \ _I ) )
84 83 eldifad 
 |-  ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) -> c e. ( Y X. Y ) )
85 elxp2 
 |-  ( c e. ( Y X. Y ) <-> E. a e. Y E. b e. Y c = <. a , b >. )
86 84 85 sylib 
 |-  ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) -> E. a e. Y E. b e. Y c = <. a , b >. )
87 82 86 r19.29vva 
 |-  ( ( ph /\ c e. ( ( Y X. Y ) \ _I ) ) -> E. z e. ( ( X X. X ) \ .~ ) ( H ` z ) = c )
88 simpr 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> z = <. x , y >. )
89 88 fveq2d 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> ( H ` z ) = ( H ` <. x , y >. ) )
90 simp-4r 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> ( H ` z ) = c )
91 simpllr 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> x e. X )
92 simplr 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> y e. X )
93 3 91 92 fvproj 
 |-  ( ( ( ( ( ( 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 ) >. )
94 89 90 93 3eqtr3d 
 |-  ( ( ( ( ( ( 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 
 |-  ( F : X -onto-> Y -> F : X --> Y )
96 5 95 syl 
 |-  ( ph -> F : X --> Y )
97 96 ad5antr 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> F : X --> Y )
98 97 91 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> ( F ` x ) e. Y )
99 97 92 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> ( F ` y ) e. Y )
100 opelxp 
 |-  ( <. ( F ` x ) , ( F ` y ) >. e. ( Y X. Y ) <-> ( ( F ` x ) e. Y /\ ( F ` y ) e. Y ) )
101 98 99 100 sylanbrc 
 |-  ( ( ( ( ( ( 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 ) )
102 simp-5r 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> z e. ( ( X X. X ) \ .~ ) )
103 88 102 eqeltrrd 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> <. x , y >. e. ( ( X X. X ) \ .~ ) )
104 58 simprbi 
 |-  ( <. x , y >. e. ( ( X X. X ) \ .~ ) -> -. x .~ y )
105 103 104 syl 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> -. x .~ y )
106 11 ad5antr 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> F Fn X )
107 106 91 92 52 syl3anc 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> ( x .~ y <-> ( F ` x ) = ( F ` y ) ) )
108 107 necon3bbid 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> ( -. x .~ y <-> ( F ` x ) =/= ( F ` y ) ) )
109 105 108 mpbid 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> ( F ` x ) =/= ( F ` y ) )
110 101 109 48 sylanbrc 
 |-  ( ( ( ( ( ( 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 ) )
111 94 110 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) /\ x e. X ) /\ y e. X ) /\ z = <. x , y >. ) -> c e. ( ( Y X. Y ) \ _I ) )
112 eldifi 
 |-  ( z e. ( ( X X. X ) \ .~ ) -> z e. ( X X. X ) )
113 112 adantl 
 |-  ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) -> z e. ( X X. X ) )
114 elxp2 
 |-  ( z e. ( X X. X ) <-> E. x e. X E. y e. X z = <. x , y >. )
115 113 114 sylib 
 |-  ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) -> E. x e. X E. y e. X z = <. x , y >. )
116 115 adantr 
 |-  ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) -> E. x e. X E. y e. X z = <. x , y >. )
117 111 116 r19.29vva 
 |-  ( ( ( ph /\ z e. ( ( X X. X ) \ .~ ) ) /\ ( H ` z ) = c ) -> c e. ( ( Y X. Y ) \ _I ) )
118 117 r19.29an 
 |-  ( ( ph /\ E. z e. ( ( X X. X ) \ .~ ) ( H ` z ) = c ) -> c e. ( ( Y X. Y ) \ _I ) )
119 87 118 impbida 
 |-  ( ph -> ( c e. ( ( Y X. Y ) \ _I ) <-> E. z e. ( ( X X. X ) \ .~ ) ( H ` z ) = c ) )
120 32 119 bitr4id 
 |-  ( ph -> ( c e. ( H " ( ( X X. X ) \ .~ ) ) <-> c e. ( ( Y X. Y ) \ _I ) ) )
121 120 eqrdv 
 |-  ( ph -> ( H " ( ( X X. X ) \ .~ ) ) = ( ( Y X. Y ) \ _I ) )
122 ssv 
 |-  Y C_ _V
123 xpss2 
 |-  ( Y C_ _V -> ( Y X. Y ) C_ ( Y X. _V ) )
124 difres 
 |-  ( ( Y X. Y ) C_ ( Y X. _V ) -> ( ( Y X. Y ) \ ( _I |` Y ) ) = ( ( Y X. Y ) \ _I ) )
125 122 123 124 mp2b 
 |-  ( ( Y X. Y ) \ ( _I |` Y ) ) = ( ( Y X. Y ) \ _I )
126 121 125 eqtr4di 
 |-  ( ph -> ( H " ( ( X X. X ) \ .~ ) ) = ( ( Y X. Y ) \ ( _I |` Y ) ) )
127 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
128 9 127 sylib 
 |-  ( ph -> J e. ( TopOn ` X ) )
129 qtoptopon 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. ( TopOn ` Y ) )
130 128 5 129 syl2anc 
 |-  ( ph -> ( J qTop F ) e. ( TopOn ` Y ) )
131 6 ralrimiva 
 |-  ( ph -> A. x e. J ( F " x ) e. ( J qTop F ) )
132 imaeq2 
 |-  ( x = y -> ( F " x ) = ( F " y ) )
133 132 eleq1d 
 |-  ( x = y -> ( ( F " x ) e. ( J qTop F ) <-> ( F " y ) e. ( J qTop F ) ) )
134 133 cbvralvw 
 |-  ( A. x e. J ( F " x ) e. ( J qTop F ) <-> A. y e. J ( F " y ) e. ( J qTop F ) )
135 131 134 sylib 
 |-  ( ph -> A. y e. J ( F " y ) e. ( J qTop F ) )
136 135 r19.21bi 
 |-  ( ( ph /\ y e. J ) -> ( F " y ) e. ( J qTop F ) )
137 1 1 txuni 
 |-  ( ( J e. Top /\ J e. Top ) -> ( X X. X ) = U. ( J tX J ) )
138 9 9 137 syl2anc 
 |-  ( ph -> ( X X. X ) = U. ( J tX J ) )
139 138 difeq1d 
 |-  ( ph -> ( ( X X. X ) \ .~ ) = ( U. ( J tX J ) \ .~ ) )
140 txtop 
 |-  ( ( J e. Top /\ J e. Top ) -> ( J tX J ) e. Top )
141 9 9 140 syl2anc 
 |-  ( ph -> ( J tX J ) e. Top )
142 fcoinver 
 |-  ( F Fn X -> ( `' F o. F ) Er X )
143 11 142 syl 
 |-  ( ph -> ( `' F o. F ) Er X )
144 ereq1 
 |-  ( .~ = ( `' F o. F ) -> ( .~ Er X <-> ( `' F o. F ) Er X ) )
145 2 144 ax-mp 
 |-  ( .~ Er X <-> ( `' F o. F ) Er X )
146 143 145 sylibr 
 |-  ( ph -> .~ Er X )
147 erssxp 
 |-  ( .~ Er X -> .~ C_ ( X X. X ) )
148 146 147 syl 
 |-  ( ph -> .~ C_ ( X X. X ) )
149 148 138 sseqtrd 
 |-  ( ph -> .~ C_ U. ( J tX J ) )
150 eqid 
 |-  U. ( J tX J ) = U. ( J tX J )
151 150 iscld2 
 |-  ( ( ( J tX J ) e. Top /\ .~ C_ U. ( J tX J ) ) -> ( .~ e. ( Clsd ` ( J tX J ) ) <-> ( U. ( J tX J ) \ .~ ) e. ( J tX J ) ) )
152 141 149 151 syl2anc 
 |-  ( ph -> ( .~ e. ( Clsd ` ( J tX J ) ) <-> ( U. ( J tX J ) \ .~ ) e. ( J tX J ) ) )
153 7 152 mpbid 
 |-  ( ph -> ( U. ( J tX J ) \ .~ ) e. ( J tX J ) )
154 139 153 eqeltrd 
 |-  ( ph -> ( ( X X. X ) \ .~ ) e. ( J tX J ) )
155 96 96 128 128 130 130 6 136 154 3 txomap 
 |-  ( ph -> ( H " ( ( X X. X ) \ .~ ) ) e. ( ( J qTop F ) tX ( J qTop F ) ) )
156 126 155 eqeltrrd 
 |-  ( ph -> ( ( Y X. Y ) \ ( _I |` Y ) ) e. ( ( J qTop F ) tX ( J qTop F ) ) )
157 27 156 eqeltrd 
 |-  ( ph -> ( U. ( ( J qTop F ) tX ( J qTop F ) ) \ ( _I |` U. ( J qTop F ) ) ) e. ( ( J qTop F ) tX ( J qTop F ) ) )
158 eqid 
 |-  U. ( ( J qTop F ) tX ( J qTop F ) ) = U. ( ( J qTop F ) tX ( J qTop F ) )
159 158 iscld2 
 |-  ( ( ( ( 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 ) ) ) )
160 159 biimpar 
 |-  ( ( ( ( ( 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 ) ) ) )
161 15 20 157 160 syl21anc 
 |-  ( ph -> ( _I |` U. ( J qTop F ) ) e. ( Clsd ` ( ( J qTop F ) tX ( J qTop F ) ) ) )
162 17 hausdiag 
 |-  ( ( J qTop F ) e. Haus <-> ( ( J qTop F ) e. Top /\ ( _I |` U. ( J qTop F ) ) e. ( Clsd ` ( ( J qTop F ) tX ( J qTop F ) ) ) ) )
163 13 161 162 sylanbrc 
 |-  ( ph -> ( J qTop F ) e. Haus )