Step | Hyp | Ref
| Expression |
1 | | pcohtpy.5 |
. . . . 5
|
2 | | isphtpc 22793 |
. . . . 5
|
3 | 1, 2 | sylib 208 |
. . . 4
|
4 | 3 | simp1d 1073 |
. . 3
|
5 | | pcohtpy.6 |
. . . . 5
|
6 | | isphtpc 22793 |
. . . . 5
|
7 | 5, 6 | sylib 208 |
. . . 4
|
8 | 7 | simp1d 1073 |
. . 3
|
9 | | pcohtpy.4 |
. . 3
|
10 | 4, 8, 9 | pcocn 22817 |
. 2
|
11 | 3 | simp2d 1074 |
. . 3
|
12 | 7 | simp2d 1074 |
. . 3
|
13 | | pcohtpylem.8 |
. . . . . 6
|
14 | 4, 11, 13 | phtpy01 22784 |
. . . . 5
|
15 | 14 | simprd 479 |
. . . 4
|
16 | | pcohtpylem.9 |
. . . . . 6
|
17 | 8, 12, 16 | phtpy01 22784 |
. . . . 5
|
18 | 17 | simpld 475 |
. . . 4
|
19 | 9, 15, 18 | 3eqtr3d 2664 |
. . 3
|
20 | 11, 12, 19 | pcocn 22817 |
. 2
|
21 | | pcohtpylem.7 |
. . 3
|
22 | | eqid 2622 |
. . . 4
|
23 | | eqid 2622 |
. . . 4
↾t ↾t |
24 | | eqid 2622 |
. . . 4
↾t ↾t |
25 | | dfii2 22685 |
. . . 4
↾t |
26 | | 0red 10041 |
. . . 4
|
27 | | 1red 10055 |
. . . 4
|
28 | | halfre 11246 |
. . . . . 6
|
29 | | 0re 10040 |
. . . . . . 7
|
30 | | halfgt0 11248 |
. . . . . . 7
|
31 | 29, 28, 30 | ltleii 10160 |
. . . . . 6
|
32 | | 1re 10039 |
. . . . . . 7
|
33 | | halflt1 11250 |
. . . . . . 7
|
34 | 28, 32, 33 | ltleii 10160 |
. . . . . 6
|
35 | 29, 32 | elicc2i 12239 |
. . . . . 6
|
36 | 28, 31, 34, 35 | mpbir3an 1244 |
. . . . 5
|
37 | 36 | a1i 11 |
. . . 4
|
38 | | iitopon 22682 |
. . . . 5
TopOn |
39 | 38 | a1i 11 |
. . . 4
TopOn |
40 | 9 | adantr 481 |
. . . . . 6
|
41 | 4, 11, 13 | phtpyi 22783 |
. . . . . . . 8
|
42 | 41 | simprd 479 |
. . . . . . 7
|
43 | 42 | adantrl 752 |
. . . . . 6
|
44 | 8, 12, 16 | phtpyi 22783 |
. . . . . . . 8
|
45 | 44 | simpld 475 |
. . . . . . 7
|
46 | 45 | adantrl 752 |
. . . . . 6
|
47 | 40, 43, 46 | 3eqtr4d 2666 |
. . . . 5
|
48 | | simprl 794 |
. . . . . . . 8
|
49 | 48 | oveq2d 6666 |
. . . . . . 7
|
50 | | 2cn 11091 |
. . . . . . . 8
|
51 | | 2ne0 11113 |
. . . . . . . 8
|
52 | 50, 51 | recidi 10756 |
. . . . . . 7
|
53 | 49, 52 | syl6eq 2672 |
. . . . . 6
|
54 | 53 | oveq1d 6665 |
. . . . 5
|
55 | 53 | oveq1d 6665 |
. . . . . . 7
|
56 | | 1m1e0 11089 |
. . . . . . 7
|
57 | 55, 56 | syl6eq 2672 |
. . . . . 6
|
58 | 57 | oveq1d 6665 |
. . . . 5
|
59 | 47, 54, 58 | 3eqtr4d 2666 |
. . . 4
|
60 | | retopon 22567 |
. . . . . . 7
TopOn |
61 | | iccssre 12255 |
. . . . . . . 8
|
62 | 29, 28, 61 | mp2an 708 |
. . . . . . 7
|
63 | | resttopon 20965 |
. . . . . . 7
TopOn
↾t TopOn |
64 | 60, 62, 63 | mp2an 708 |
. . . . . 6
↾t TopOn |
65 | 64 | a1i 11 |
. . . . 5
↾t TopOn |
66 | 65, 39 | cnmpt1st 21471 |
. . . . . 6
↾t
↾t |
67 | 23 | iihalf1cn 22731 |
. . . . . . 7
↾t |
68 | 67 | a1i 11 |
. . . . . 6
↾t |
69 | | oveq2 6658 |
. . . . . 6
|
70 | 65, 39, 66, 65, 68, 69 | cnmpt21 21474 |
. . . . 5
↾t
|
71 | 65, 39 | cnmpt2nd 21472 |
. . . . 5
↾t
|
72 | 4, 11 | phtpycn 22782 |
. . . . . 6
|
73 | 72, 13 | sseldd 3604 |
. . . . 5
|
74 | 65, 39, 70, 71, 73 | cnmpt22f 21478 |
. . . 4
↾t
|
75 | | iccssre 12255 |
. . . . . . . 8
|
76 | 28, 32, 75 | mp2an 708 |
. . . . . . 7
|
77 | | resttopon 20965 |
. . . . . . 7
TopOn
↾t TopOn |
78 | 60, 76, 77 | mp2an 708 |
. . . . . 6
↾t TopOn |
79 | 78 | a1i 11 |
. . . . 5
↾t TopOn |
80 | 79, 39 | cnmpt1st 21471 |
. . . . . 6
↾t
↾t |
81 | 24 | iihalf2cn 22733 |
. . . . . . 7
↾t |
82 | 81 | a1i 11 |
. . . . . 6
↾t |
83 | 69 | oveq1d 6665 |
. . . . . 6
|
84 | 79, 39, 80, 79, 82, 83 | cnmpt21 21474 |
. . . . 5
↾t
|
85 | 79, 39 | cnmpt2nd 21472 |
. . . . 5
↾t
|
86 | 8, 12 | phtpycn 22782 |
. . . . . 6
|
87 | 86, 16 | sseldd 3604 |
. . . . 5
|
88 | 79, 39, 84, 85, 87 | cnmpt22f 21478 |
. . . 4
↾t
|
89 | 22, 23, 24, 25, 26, 27, 37, 39, 59, 74, 88 | cnmpt2pc 22727 |
. . 3
|
90 | 21, 89 | syl5eqel 2705 |
. 2
|
91 | | simpll 790 |
. . . . . . 7
|
92 | | elii1 22734 |
. . . . . . . . 9
|
93 | | iihalf1 22730 |
. . . . . . . . 9
|
94 | 92, 93 | sylbir 225 |
. . . . . . . 8
|
95 | 94 | adantll 750 |
. . . . . . 7
|
96 | 4, 11 | phtpyhtpy 22781 |
. . . . . . . . 9
Htpy |
97 | 96, 13 | sseldd 3604 |
. . . . . . . 8
Htpy |
98 | 39, 4, 11, 97 | htpyi 22773 |
. . . . . . 7
|
99 | 91, 95, 98 | syl2anc 693 |
. . . . . 6
|
100 | 99 | simpld 475 |
. . . . 5
|
101 | | iftrue 4092 |
. . . . . 6
|
102 | 101 | adantl 482 |
. . . . 5
|
103 | | iftrue 4092 |
. . . . . 6
|
104 | 103 | adantl 482 |
. . . . 5
|
105 | 100, 102,
104 | 3eqtr4d 2666 |
. . . 4
|
106 | | simpll 790 |
. . . . . . 7
|
107 | | elii2 22735 |
. . . . . . . . 9
|
108 | 107 | adantll 750 |
. . . . . . . 8
|
109 | | iihalf2 22732 |
. . . . . . . 8
|
110 | 108, 109 | syl 17 |
. . . . . . 7
|
111 | 8, 12 | phtpyhtpy 22781 |
. . . . . . . . 9
Htpy |
112 | 111, 16 | sseldd 3604 |
. . . . . . . 8
Htpy |
113 | 39, 8, 12, 112 | htpyi 22773 |
. . . . . . 7
|
114 | 106, 110,
113 | syl2anc 693 |
. . . . . 6
|
115 | 114 | simpld 475 |
. . . . 5
|
116 | | iffalse 4095 |
. . . . . 6
|
117 | 116 | adantl 482 |
. . . . 5
|
118 | | iffalse 4095 |
. . . . . 6
|
119 | 118 | adantl 482 |
. . . . 5
|
120 | 115, 117,
119 | 3eqtr4d 2666 |
. . . 4
|
121 | 105, 120 | pm2.61dan 832 |
. . 3
|
122 | | simpr 477 |
. . . 4
|
123 | | 0elunit 12290 |
. . . 4
|
124 | | simpl 473 |
. . . . . . 7
|
125 | 124 | breq1d 4663 |
. . . . . 6
|
126 | 124 | oveq2d 6666 |
. . . . . . 7
|
127 | | simpr 477 |
. . . . . . 7
|
128 | 126, 127 | oveq12d 6668 |
. . . . . 6
|
129 | 126 | oveq1d 6665 |
. . . . . . 7
|
130 | 129, 127 | oveq12d 6668 |
. . . . . 6
|
131 | 125, 128,
130 | ifbieq12d 4113 |
. . . . 5
|
132 | | ovex 6678 |
. . . . . 6
|
133 | | ovex 6678 |
. . . . . 6
|
134 | 132, 133 | ifex 4156 |
. . . . 5
|
135 | 131, 21, 134 | ovmpt2a 6791 |
. . . 4
|
136 | 122, 123,
135 | sylancl 694 |
. . 3
|
137 | 4, 8 | pcovalg 22812 |
. . 3
|
138 | 121, 136,
137 | 3eqtr4d 2666 |
. 2
|
139 | 99 | simprd 479 |
. . . . 5
|
140 | | iftrue 4092 |
. . . . . 6
|
141 | 140 | adantl 482 |
. . . . 5
|
142 | | iftrue 4092 |
. . . . . 6
|
143 | 142 | adantl 482 |
. . . . 5
|
144 | 139, 141,
143 | 3eqtr4d 2666 |
. . . 4
|
145 | 114 | simprd 479 |
. . . . 5
|
146 | | iffalse 4095 |
. . . . . 6
|
147 | 146 | adantl 482 |
. . . . 5
|
148 | | iffalse 4095 |
. . . . . 6
|
149 | 148 | adantl 482 |
. . . . 5
|
150 | 145, 147,
149 | 3eqtr4d 2666 |
. . . 4
|
151 | 144, 150 | pm2.61dan 832 |
. . 3
|
152 | | 1elunit 12291 |
. . . 4
|
153 | | simpl 473 |
. . . . . . 7
|
154 | 153 | breq1d 4663 |
. . . . . 6
|
155 | 153 | oveq2d 6666 |
. . . . . . 7
|
156 | | simpr 477 |
. . . . . . 7
|
157 | 155, 156 | oveq12d 6668 |
. . . . . 6
|
158 | 155 | oveq1d 6665 |
. . . . . . 7
|
159 | 158, 156 | oveq12d 6668 |
. . . . . 6
|
160 | 154, 157,
159 | ifbieq12d 4113 |
. . . . 5
|
161 | | ovex 6678 |
. . . . . 6
|
162 | | ovex 6678 |
. . . . . 6
|
163 | 161, 162 | ifex 4156 |
. . . . 5
|
164 | 160, 21, 163 | ovmpt2a 6791 |
. . . 4
|
165 | 122, 152,
164 | sylancl 694 |
. . 3
|
166 | 11, 12 | pcovalg 22812 |
. . 3
|
167 | 151, 165,
166 | 3eqtr4d 2666 |
. 2
|
168 | 4, 11, 13 | phtpyi 22783 |
. . . 4
|
169 | 168 | simpld 475 |
. . 3
|
170 | | simpl 473 |
. . . . . . . 8
|
171 | 170, 31 | syl6eqbr 4692 |
. . . . . . 7
|
172 | 171 | iftrued 4094 |
. . . . . 6
|
173 | 170 | oveq2d 6666 |
. . . . . . . 8
|
174 | | 2t0e0 11183 |
. . . . . . . 8
|
175 | 173, 174 | syl6eq 2672 |
. . . . . . 7
|
176 | | simpr 477 |
. . . . . . 7
|
177 | 175, 176 | oveq12d 6668 |
. . . . . 6
|
178 | 172, 177 | eqtrd 2656 |
. . . . 5
|
179 | | ovex 6678 |
. . . . 5
|
180 | 178, 21, 179 | ovmpt2a 6791 |
. . . 4
|
181 | 123, 122,
180 | sylancr 695 |
. . 3
|
182 | 4, 8 | pco0 22814 |
. . . 4
|
183 | 182 | adantr 481 |
. . 3
|
184 | 169, 181,
183 | 3eqtr4d 2666 |
. 2
|
185 | 8, 12, 16 | phtpyi 22783 |
. . . 4
|
186 | 185 | simprd 479 |
. . 3
|
187 | 28, 32 | ltnlei 10158 |
. . . . . . . . 9
|
188 | 33, 187 | mpbi 220 |
. . . . . . . 8
|
189 | | simpl 473 |
. . . . . . . . 9
|
190 | 189 | breq1d 4663 |
. . . . . . . 8
|
191 | 188, 190 | mtbiri 317 |
. . . . . . 7
|
192 | 191 | iffalsed 4097 |
. . . . . 6
|
193 | 189 | oveq2d 6666 |
. . . . . . . . . 10
|
194 | | 2t1e2 11176 |
. . . . . . . . . 10
|
195 | 193, 194 | syl6eq 2672 |
. . . . . . . . 9
|
196 | 195 | oveq1d 6665 |
. . . . . . . 8
|
197 | | 2m1e1 11135 |
. . . . . . . 8
|
198 | 196, 197 | syl6eq 2672 |
. . . . . . 7
|
199 | | simpr 477 |
. . . . . . 7
|
200 | 198, 199 | oveq12d 6668 |
. . . . . 6
|
201 | 192, 200 | eqtrd 2656 |
. . . . 5
|
202 | | ovex 6678 |
. . . . 5
|
203 | 201, 21, 202 | ovmpt2a 6791 |
. . . 4
|
204 | 152, 122,
203 | sylancr 695 |
. . 3
|
205 | 4, 8 | pco1 22815 |
. . . 4
|
206 | 205 | adantr 481 |
. . 3
|
207 | 186, 204,
206 | 3eqtr4d 2666 |
. 2
|
208 | 10, 20, 90, 138, 167, 184, 207 | isphtpy2d 22786 |
1
|