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 = J
qtophaus.e ˙ = F -1 F
qtophaus.h H = x X , y X F x F y
qtophaus.1 φ J Haus
qtophaus.2 φ F : X onto Y
qtophaus.3 φ x J F x J qTop F
qtophaus.4 φ ˙ Clsd J × t J
Assertion qtophaus φ J qTop F Haus

Proof

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