Metamath Proof Explorer


Theorem qtoprest

Description: If A is a saturated open or closed set (where saturated means that A = (`' F " U ) for some U ), then the restriction of the quotient map F to A ` is a quotient map. (Contributed by Mario Carneiro, 24-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses qtoprest.2 φ J TopOn X
qtoprest.3 φ F : X onto Y
qtoprest.4 φ U Y
qtoprest.5 φ A = F -1 U
qtoprest.6 φ A J A Clsd J
Assertion qtoprest φ J qTop F 𝑡 U = J 𝑡 A qTop F A

Proof

Step Hyp Ref Expression
1 qtoprest.2 φ J TopOn X
2 qtoprest.3 φ F : X onto Y
3 qtoprest.4 φ U Y
4 qtoprest.5 φ A = F -1 U
5 qtoprest.6 φ A J A Clsd J
6 fofn F : X onto Y F Fn X
7 2 6 syl φ F Fn X
8 qtopid J TopOn X F Fn X F J Cn J qTop F
9 1 7 8 syl2anc φ F J Cn J qTop F
10 cnvimass F -1 U dom F
11 7 fndmd φ dom F = X
12 10 11 sseqtrid φ F -1 U X
13 4 12 eqsstrd φ A X
14 toponuni J TopOn X X = J
15 1 14 syl φ X = J
16 13 15 sseqtrd φ A J
17 eqid J = J
18 17 cnrest F J Cn J qTop F A J F A J 𝑡 A Cn J qTop F
19 9 16 18 syl2anc φ F A J 𝑡 A Cn J qTop F
20 qtoptopon J TopOn X F : X onto Y J qTop F TopOn Y
21 1 2 20 syl2anc φ J qTop F TopOn Y
22 df-ima F A = ran F A
23 4 imaeq2d φ F A = F F -1 U
24 foimacnv F : X onto Y U Y F F -1 U = U
25 2 3 24 syl2anc φ F F -1 U = U
26 23 25 eqtrd φ F A = U
27 22 26 eqtr3id φ ran F A = U
28 eqimss ran F A = U ran F A U
29 27 28 syl φ ran F A U
30 cnrest2 J qTop F TopOn Y ran F A U U Y F A J 𝑡 A Cn J qTop F F A J 𝑡 A Cn J qTop F 𝑡 U
31 21 29 3 30 syl3anc φ F A J 𝑡 A Cn J qTop F F A J 𝑡 A Cn J qTop F 𝑡 U
32 19 31 mpbid φ F A J 𝑡 A Cn J qTop F 𝑡 U
33 resttopon J qTop F TopOn Y U Y J qTop F 𝑡 U TopOn U
34 21 3 33 syl2anc φ J qTop F 𝑡 U TopOn U
35 qtopss F A J 𝑡 A Cn J qTop F 𝑡 U J qTop F 𝑡 U TopOn U ran F A = U J qTop F 𝑡 U J 𝑡 A qTop F A
36 32 34 27 35 syl3anc φ J qTop F 𝑡 U J 𝑡 A qTop F A
37 resttopon J TopOn X A X J 𝑡 A TopOn A
38 1 13 37 syl2anc φ J 𝑡 A TopOn A
39 fnfun F Fn X Fun F
40 7 39 syl φ Fun F
41 13 11 sseqtrrd φ A dom F
42 fores Fun F A dom F F A : A onto F A
43 40 41 42 syl2anc φ F A : A onto F A
44 foeq3 F A = U F A : A onto F A F A : A onto U
45 26 44 syl φ F A : A onto F A F A : A onto U
46 43 45 mpbid φ F A : A onto U
47 elqtop3 J 𝑡 A TopOn A F A : A onto U x J 𝑡 A qTop F A x U F A -1 x J 𝑡 A
48 38 46 47 syl2anc φ x J 𝑡 A qTop F A x U F A -1 x J 𝑡 A
49 cnvresima F A -1 x = F -1 x A
50 imass2 x U F -1 x F -1 U
51 50 adantl φ x U F -1 x F -1 U
52 4 adantr φ x U A = F -1 U
53 51 52 sseqtrrd φ x U F -1 x A
54 df-ss F -1 x A F -1 x A = F -1 x
55 53 54 sylib φ x U F -1 x A = F -1 x
56 49 55 syl5eq φ x U F A -1 x = F -1 x
57 56 eleq1d φ x U F A -1 x J 𝑡 A F -1 x J 𝑡 A
58 simplrl φ x U F -1 x J 𝑡 A A J x U
59 df-ss x U x U = x
60 58 59 sylib φ x U F -1 x J 𝑡 A A J x U = x
61 topontop J qTop F TopOn Y J qTop F Top
62 21 61 syl φ J qTop F Top
63 62 ad2antrr φ x U F -1 x J 𝑡 A A J J qTop F Top
64 toponmax J TopOn X X J
65 1 64 syl φ X J
66 fornex X J F : X onto Y Y V
67 65 2 66 sylc φ Y V
68 67 3 ssexd φ U V
69 68 ad2antrr φ x U F -1 x J 𝑡 A A J U V
70 3 ad2antrr φ x U F -1 x J 𝑡 A A J U Y
71 58 70 sstrd φ x U F -1 x J 𝑡 A A J x Y
72 topontop J TopOn X J Top
73 1 72 syl φ J Top
74 restopn2 J Top A J F -1 x J 𝑡 A F -1 x J F -1 x A
75 73 74 sylan φ A J F -1 x J 𝑡 A F -1 x J F -1 x A
76 75 simprbda φ A J F -1 x J 𝑡 A F -1 x J
77 76 adantrl φ A J x U F -1 x J 𝑡 A F -1 x J
78 77 an32s φ x U F -1 x J 𝑡 A A J F -1 x J
79 elqtop3 J TopOn X F : X onto Y x J qTop F x Y F -1 x J
80 1 2 79 syl2anc φ x J qTop F x Y F -1 x J
81 80 ad2antrr φ x U F -1 x J 𝑡 A A J x J qTop F x Y F -1 x J
82 71 78 81 mpbir2and φ x U F -1 x J 𝑡 A A J x J qTop F
83 elrestr J qTop F Top U V x J qTop F x U J qTop F 𝑡 U
84 63 69 82 83 syl3anc φ x U F -1 x J 𝑡 A A J x U J qTop F 𝑡 U
85 60 84 eqeltrrd φ x U F -1 x J 𝑡 A A J x J qTop F 𝑡 U
86 34 ad2antrr φ x U F -1 x J 𝑡 A A Clsd J J qTop F 𝑡 U TopOn U
87 toponuni J qTop F 𝑡 U TopOn U U = J qTop F 𝑡 U
88 86 87 syl φ x U F -1 x J 𝑡 A A Clsd J U = J qTop F 𝑡 U
89 88 difeq1d φ x U F -1 x J 𝑡 A A Clsd J U x = J qTop F 𝑡 U x
90 3 ad2antrr φ x U F -1 x J 𝑡 A A Clsd J U Y
91 21 ad2antrr φ x U F -1 x J 𝑡 A A Clsd J J qTop F TopOn Y
92 toponuni J qTop F TopOn Y Y = J qTop F
93 91 92 syl φ x U F -1 x J 𝑡 A A Clsd J Y = J qTop F
94 90 93 sseqtrd φ x U F -1 x J 𝑡 A A Clsd J U J qTop F
95 90 ssdifssd φ x U F -1 x J 𝑡 A A Clsd J U x Y
96 40 ad2antrr φ x U F -1 x J 𝑡 A A Clsd J Fun F
97 funcnvcnv Fun F Fun F -1 -1
98 imadif Fun F -1 -1 F -1 U x = F -1 U F -1 x
99 96 97 98 3syl φ x U F -1 x J 𝑡 A A Clsd J F -1 U x = F -1 U F -1 x
100 4 ad2antrr φ x U F -1 x J 𝑡 A A Clsd J A = F -1 U
101 100 difeq1d φ x U F -1 x J 𝑡 A A Clsd J A F -1 x = F -1 U F -1 x
102 99 101 eqtr4d φ x U F -1 x J 𝑡 A A Clsd J F -1 U x = A F -1 x
103 simpr φ x U F -1 x J 𝑡 A A Clsd J A Clsd J
104 38 ad2antrr φ x U F -1 x J 𝑡 A A Clsd J J 𝑡 A TopOn A
105 toponuni J 𝑡 A TopOn A A = J 𝑡 A
106 104 105 syl φ x U F -1 x J 𝑡 A A Clsd J A = J 𝑡 A
107 106 difeq1d φ x U F -1 x J 𝑡 A A Clsd J A F -1 x = J 𝑡 A F -1 x
108 topontop J 𝑡 A TopOn A J 𝑡 A Top
109 104 108 syl φ x U F -1 x J 𝑡 A A Clsd J J 𝑡 A Top
110 simplrr φ x U F -1 x J 𝑡 A A Clsd J F -1 x J 𝑡 A
111 eqid J 𝑡 A = J 𝑡 A
112 111 opncld J 𝑡 A Top F -1 x J 𝑡 A J 𝑡 A F -1 x Clsd J 𝑡 A
113 109 110 112 syl2anc φ x U F -1 x J 𝑡 A A Clsd J J 𝑡 A F -1 x Clsd J 𝑡 A
114 107 113 eqeltrd φ x U F -1 x J 𝑡 A A Clsd J A F -1 x Clsd J 𝑡 A
115 restcldr A Clsd J A F -1 x Clsd J 𝑡 A A F -1 x Clsd J
116 103 114 115 syl2anc φ x U F -1 x J 𝑡 A A Clsd J A F -1 x Clsd J
117 102 116 eqeltrd φ x U F -1 x J 𝑡 A A Clsd J F -1 U x Clsd J
118 qtopcld J TopOn X F : X onto Y U x Clsd J qTop F U x Y F -1 U x Clsd J
119 1 2 118 syl2anc φ U x Clsd J qTop F U x Y F -1 U x Clsd J
120 119 ad2antrr φ x U F -1 x J 𝑡 A A Clsd J U x Clsd J qTop F U x Y F -1 U x Clsd J
121 95 117 120 mpbir2and φ x U F -1 x J 𝑡 A A Clsd J U x Clsd J qTop F
122 difssd φ x U F -1 x J 𝑡 A A Clsd J U x U
123 eqid J qTop F = J qTop F
124 123 restcldi U J qTop F U x Clsd J qTop F U x U U x Clsd J qTop F 𝑡 U
125 94 121 122 124 syl3anc φ x U F -1 x J 𝑡 A A Clsd J U x Clsd J qTop F 𝑡 U
126 89 125 eqeltrrd φ x U F -1 x J 𝑡 A A Clsd J J qTop F 𝑡 U x Clsd J qTop F 𝑡 U
127 topontop J qTop F 𝑡 U TopOn U J qTop F 𝑡 U Top
128 86 127 syl φ x U F -1 x J 𝑡 A A Clsd J J qTop F 𝑡 U Top
129 simplrl φ x U F -1 x J 𝑡 A A Clsd J x U
130 129 88 sseqtrd φ x U F -1 x J 𝑡 A A Clsd J x J qTop F 𝑡 U
131 eqid J qTop F 𝑡 U = J qTop F 𝑡 U
132 131 isopn2 J qTop F 𝑡 U Top x J qTop F 𝑡 U x J qTop F 𝑡 U J qTop F 𝑡 U x Clsd J qTop F 𝑡 U
133 128 130 132 syl2anc φ x U F -1 x J 𝑡 A A Clsd J x J qTop F 𝑡 U J qTop F 𝑡 U x Clsd J qTop F 𝑡 U
134 126 133 mpbird φ x U F -1 x J 𝑡 A A Clsd J x J qTop F 𝑡 U
135 5 adantr φ x U F -1 x J 𝑡 A A J A Clsd J
136 85 134 135 mpjaodan φ x U F -1 x J 𝑡 A x J qTop F 𝑡 U
137 136 expr φ x U F -1 x J 𝑡 A x J qTop F 𝑡 U
138 57 137 sylbid φ x U F A -1 x J 𝑡 A x J qTop F 𝑡 U
139 138 expimpd φ x U F A -1 x J 𝑡 A x J qTop F 𝑡 U
140 48 139 sylbid φ x J 𝑡 A qTop F A x J qTop F 𝑡 U
141 140 ssrdv φ J 𝑡 A qTop F A J qTop F 𝑡 U
142 36 141 eqssd φ J qTop F 𝑡 U = J 𝑡 A qTop F A