# 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}=\bigcup {J}$
qtophaus.e
qtophaus.h ${⊢}{H}=\left({x}\in {X},{y}\in {X}⟼⟨{F}\left({x}\right),{F}\left({y}\right)⟩\right)$
qtophaus.1 ${⊢}{\phi }\to {J}\in \mathrm{Haus}$
qtophaus.2 ${⊢}{\phi }\to {F}:{X}\underset{onto}{⟶}{Y}$
qtophaus.3 ${⊢}\left({\phi }\wedge {x}\in {J}\right)\to {F}\left[{x}\right]\in \left({J}\mathrm{qTop}{F}\right)$
qtophaus.4
Assertion qtophaus ${⊢}{\phi }\to {J}\mathrm{qTop}{F}\in \mathrm{Haus}$

### Proof

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