Nearby theorems
|
|
Mathbox for Brendan Leahy |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > poimir | Structured version Visualization version Unicode version | ||
| Description: Poincare-Miranda theorem. Theorem on [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
| Ref | Expression |
|---|---|
| poimir.0 |
        |
| poimir.i |
   ![[,]](_icc.gif "[,]"){kind=small}    |
| poimir.r |
         |
| poimir.1 |
 ↾t  |
| poimir.2 |
![/\](wedge.gif "/\"){kind=small}
  |
| poimir.3 |
|
| Ref | Expression |
|---|---|
| poimir |
  |
,, ,
, , , , ,,,
, ,,, , ,,,
are
mutually distinct and distinct from all other variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | poimir.0 |
. . 3
| |
| 2 | poimir.i |
. . 3
| |
| 3 | poimir.r |
. . 3
| |
| 4 | poimir.1 |
. . 3
↾t | |
| 5 | poimir.2 |
. . 3
| |
| 6 | poimir.3 |
. . 3
| |
| 7 | 1, 2, 3, 4, 5, 6 | poimirlem32 32036 |
. 2
↾t
  |
| 8 | ovex 6336 |
. . . . . . . . . . . . . . . . . . . . . 22
 | |
| 9 | retopon 21862 |
. . . . . . . . . . . . . . . . . . . . . 22
TopOn | |
| 10 | 3 | pttoponconst 20689 |
. . . . . . . . . . . . . . . . . . . . . 22
TopOn
TopOn |
| 11 | 8, 9, 10 | mp2an 686 |
. . . . . . . . . . . . . . . . . . . . 21
TopOn |
| 12 | 11 | topontopi 20023 |
. . . . . . . . . . . . . . . . . . . 20
 |
| 13 | reex 9648 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 14 | unitssre 11805 |
. . . . . . . . . . . . . . . . . . . . . 22
 | |
| 15 | mapss 7532 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 16 | 13, 14, 15 | mp2an 686 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 17 | 2, 16 | eqsstri 3448 |
. . . . . . . . . . . . . . . . . . . 20
|
| 18 | 11 | toponunii 20024 |
. . . . . . . . . . . . . . . . . . . . 21
 |
| 19 | 18 | restuni 20255 |
. . . . . . . . . . . . . . . . . . . 20
↾t |
| 20 | 12, 17, 19 | mp2an 686 |
. . . . . . . . . . . . . . . . . . 19
↾t |
| 21 | 20, 18 | cnf 20339 |
. . . . . . . . . . . . . . . . . 18
↾t   |
| 22 | 4, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
| 23 | 22 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . 16
|
| 24 | elmapi 7511 |
. . . . . . . . . . . . . . . 16
| |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . 15
|
| 26 | 25 | ffvelrnda 6037 |
. . . . . . . . . . . . . 14
|
| 27 | recn 9647 |
. . . . . . . . . . . . . . . . 17
 | |
| 28 | absrpcl 13428 |
. . . . . . . . . . . . . . . . . 18
   | |
| 29 | 28 | ex 441 |
. . . . . . . . . . . . . . . . 17
|
| 30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
|
| 31 | ltsubrp 11358 |
. . . . . . . . . . . . . . . . . 18
  | |
| 32 | ltaddrp 11359 |
. . . . . . . . . . . . . . . . . 18
 | |
| 33 | 31, 32 | jca 541 |
. . . . . . . . . . . . . . . . 17
|
| 34 | 33 | ex 441 |
. . . . . . . . . . . . . . . 16
|
| 35 | 30, 34 | syld 44 |
. . . . . . . . . . . . . . 15
|
| 36 | 27 | abscld 13575 |
. . . . . . . . . . . . . . . . . 18
|
| 37 | resubcl 9958 |
. . . . . . . . . . . . . . . . . 18
| |
| 38 | 36, 37 | mpdan 681 |
. . . . . . . . . . . . . . . . 17
|
| 39 | 38 | rexrd 9708 |
. . . . . . . . . . . . . . . 16
 |
| 40 | readdcl 9640 |
. . . . . . . . . . . . . . . . . 18
| |
| 41 | 36, 40 | mpdan 681 |
. . . . . . . . . . . . . . . . 17
|
| 42 | 41 | rexrd 9708 |
. . . . . . . . . . . . . . . 16
|
| 43 | rexr 9704 |
. . . . . . . . . . . . . . . 16
| |
| 44 | elioo5 11717 |
. . . . . . . . . . . . . . . 16
| |
| 45 | 39, 42, 43, 44 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
|
| 46 | 35, 45 | sylibrd 242 |
. . . . . . . . . . . . . 14
|
| 47 | 26, 46 | syl 17 |
. . . . . . . . . . . . 13
|
| 48 | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
| |
| 49 | 48 | fveq1d 5881 |
. . . . . . . . . . . . . . . 16
|
| 50 | eqid 2471 |
. . . . . . . . . . . . . . . 16
 | |
| 51 | fvex 5889 |
. . . . . . . . . . . . . . . 16
| |
| 52 | 49, 50, 51 | fvmpt 5963 |
. . . . . . . . . . . . . . 15
|
| 53 | 52 | eleq1d 2533 |
. . . . . . . . . . . . . 14
|
| 54 | 53 | ad2antlr 741 |
. . . . . . . . . . . . 13
|
| 55 | 47, 54 | sylibrd 242 |
. . . . . . . . . . . 12
|
| 56 | iooretop 21864 |
. . . . . . . . . . . . 13
| |
| 57 | resttopon 20254 |
. . . . . . . . . . . . . . . . . . . 20
TopOn
↾t TopOn | |
| 58 | 11, 17, 57 | mp2an 686 |
. . . . . . . . . . . . . . . . . . 19
↾t TopOn |
| 59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
↾t TopOn |
| 60 | 22 | feqmptd 5932 |
. . . . . . . . . . . . . . . . . . . 20
|
| 61 | 60, 4 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . . . 19
↾t |
| 62 | 61 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
↾t |
| 63 | 11 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
TopOn |
| 64 | retop 21860 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 65 | 64 | fconst6 5786 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 66 | 18, 3 | ptpjcn 20703 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 67 | 8, 65, 66 | mp3an12 1380 |
. . . . . . . . . . . . . . . . . . . 20
|
| 68 | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 69 | 68 | fvconst2 6136 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 70 | 69 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . 20
|
| 71 | 67, 70 | eleqtrd 2551 |
. . . . . . . . . . . . . . . . . . 19
|
| 72 | 71 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
|
| 73 | fveq1 5878 |
. . . . . . . . . . . . . . . . . 18
| |
| 74 | 59, 62, 63, 72, 73 | cnmpt11 20755 |
. . . . . . . . . . . . . . . . 17
↾t
|
| 75 | 20 | cncnpi 20371 |
. . . . . . . . . . . . . . . . 17
↾t
↾t 
|
| 76 | 74, 75 | sylan 479 |
. . . . . . . . . . . . . . . 16
↾t
|
| 77 | 76 | an32s 821 |
. . . . . . . . . . . . . . 15
↾t
|
| 78 | iscnp 20330 |
. . . . . . . . . . . . . . . . 17
↾t TopOn
TopOn
↾t
↾t 
| |
| 79 | 58, 9, 78 | mp3an12 1380 |
. . . . . . . . . . . . . . . 16
↾t
↾t
|
| 80 | 79 | ad2antlr 741 |
. . . . . . . . . . . . . . 15
↾t
↾t
|
| 81 | 77, 80 | mpbid 215 |
. . . . . . . . . . . . . 14
↾t
|
| 82 | 81 | simprd 470 |
. . . . . . . . . . . . 13
↾t
|
| 83 | eleq2 2538 |
. . . . . . . . . . . . . . 15
| |
| 84 | sseq2 3440 |
. . . . . . . . . . . . . . . . 17
| |
| 85 | 84 | anbi2d 718 |
. . . . . . . . . . . . . . . 16
|
| 86 | 85 | rexbidv 2892 |
. . . . . . . . . . . . . . 15
↾t
↾t |
| 87 | 83, 86 | imbi12d 327 |
. . . . . . . . . . . . . 14
↾t
↾t
|
| 88 | 87 | rspcv 3132 |
. . . . . . . . . . . . 13
↾t
↾t
|
| 89 | 56, 82, 88 | mpsyl 64 |
. . . . . . . . . . . 12
↾t
|
| 90 | 55, 89 | syld 44 |
. . . . . . . . . . 11
↾t
|
| 91 | 0re 9661 |
. . . . . . . . . . . 12
| |
| 92 | letric 9752 |
. . . . . . . . . . . 12
| |
| 93 | 26, 91, 92 | sylancl 675 |
. . . . . . . . . . 11
|
| 94 | 90, 93 | jctird 553 |
. . . . . . . . . 10
↾t
|
| 95 | r19.41v 2928 |
. . . . . . . . . . 11
↾t
↾t
| |
| 96 | anass 661 |
. . . . . . . . . . . 12
| |
| 97 | 96 | rexbii 2881 |
. . . . . . . . . . 11
↾t
↾t
|
| 98 | 95, 97 | bitr3i 259 |
. . . . . . . . . 10
↾t
↾t
|
| 99 | 94, 98 | syl6ib 234 |
. . . . . . . . 9
↾t
|
| 100 | 58 | topontopi 20023 |
. . . . . . . . . . . . 13
↾t |
| 101 | 20 | eltopss 20014 |
. . . . . . . . . . . . 13
↾t ↾t |
| 102 | 100, 101 | mpan 684 |
. . . . . . . . . . . 12
↾t |
| 103 | fvex 5889 |
. . . . . . . . . . . . . . . . . 18
| |
| 104 | 103, 50 | dmmpti 5717 |
. . . . . . . . . . . . . . . . 17
 |
| 105 | 104 | sseq2i 3443 |
. . . . . . . . . . . . . . . 16
|
| 106 | funmpt 5625 |
. . . . . . . . . . . . . . . . 17
 | |
| 107 | funimass4 5930 |
. . . . . . . . . . . . . . . . 17
| |
| 108 | 106, 107 | mpan 684 |
. . . . . . . . . . . . . . . 16
|
| 109 | 105, 108 | sylbir 218 |
. . . . . . . . . . . . . . 15
|
| 110 | ssel2 3413 |
. . . . . . . . . . . . . . . . 17
| |
| 111 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 112 | 111 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . . 20
|
| 113 | fvex 5889 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 114 | 112, 50, 113 | fvmpt 5963 |
. . . . . . . . . . . . . . . . . . 19
|
| 115 | 114 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
|
| 116 | eliooord 11719 |
. . . . . . . . . . . . . . . . . 18
| |
| 117 | 115, 116 | syl6bi 236 |
. . . . . . . . . . . . . . . . 17
|
| 118 | 110, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
|
| 119 | 118 | ralimdva 2805 |
. . . . . . . . . . . . . . 15
|
| 120 | 109, 119 | sylbid 223 |
. . . . . . . . . . . . . 14
|
| 121 | 120 | adantl 473 |
. . . . . . . . . . . . 13
|
| 122 | absnid 13438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 | |
| 123 | 122 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 124 | 27 | negidd 9995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 125 | 124 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 126 | 123, 125 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 127 | 26, 126 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 128 | 127 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 129 | 128 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 130 | 22 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 131 | elmapi 7511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 133 | 132 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 134 | 133 | an32s 821 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 135 | 0red 9662 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
| |
| 136 | 134, 135 | ltnled 9799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
| 137 | 136 | adantllr 733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 138 | 137 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 139 | 129, 138 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 140 | 139 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 141 | 110, 140 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . 20
|
| 142 | 141 | anassrs 660 |
. . . . . . . . . . . . . . . . . . 19
|
| 143 | 142 | adantld 474 |
. . . . . . . . . . . . . . . . . 18
|
| 144 | 143 | ralimdva 2805 |
. . . . . . . . . . . . . . . . 17
|
| 145 | 144 | an32s 821 |
. . . . . . . . . . . . . . . 16
|
| 146 | 145 | impancom 447 |
. . . . . . . . . . . . . . 15
|
| 147 | absid 13436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 148 | 147 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 149 | 27 | subidd 9993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 150 | 149 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 151 | 148, 150 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 152 | 26, 151 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 153 | 152 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 154 | 153 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 155 | 135, 134 | ltnled 9799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 156 | 155 | adantllr 733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 157 | 156 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 158 | 154, 157 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 159 | 158 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 160 | 110, 159 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . 20
|
| 161 | 160 | anassrs 660 |
. . . . . . . . . . . . . . . . . . 19
|
| 162 | 161 | adantrd 475 |
. . . . . . . . . . . . . . . . . 18
|
| 163 | 162 | ralimdva 2805 |
. . . . . . . . . . . . . . . . 17
|
| 164 | 163 | an32s 821 |
. . . . . . . . . . . . . . . 16
|
| 165 | 164 | impancom 447 |
. . . . . . . . . . . . . . 15
|
| 166 | 146, 165 | orim12d 856 |
. . . . . . . . . . . . . 14
|
| 167 | 166 | expimpd 614 |
. . . . . . . . . . . . 13
|
| 168 | 121, 167 | syland 489 |
. . . . . . . . . . . 12
|
| 169 | 102, 168 | sylan2 482 |
. . . . . . . . . . 11
↾t
|
| 170 | 169 | anim2d 575 |
. . . . . . . . . 10
↾t
|
| 171 | 170 | reximdva 2858 |
. . . . . . . . 9
↾t
↾t
|
| 172 | 99, 171 | syld 44 |
. . . . . . . 8
↾t
|
| 173 | ralnex 2834 |
. . . . . . . . . . . . . 14
| |
| 174 | 173 | rexbii 2881 |
. . . . . . . . . . . . 13
|
| 175 | letsr 16551 |
. . . . . . . . . . . . . . 15
 | |
| 176 | 175 | elexi 3041 |
. . . . . . . . . . . . . 14
|
| 177 | 176 | cnvex 6759 |
. . . . . . . . . . . . . 14
|
| 178 | breq 4397 |
. . . . . . . . . . . . . . . 16
| |
| 179 | 178 | notbid 301 |
. . . . . . . . . . . . . . 15
|
| 180 | 179 | ralbidv 2829 |
. . . . . . . . . . . . . 14
|
| 181 | breq 4397 |
. . . . . . . . . . . . . . . . 17
| |
| 182 | c0ex 9655 |
. . . . . . . . . . . . . . . . . 18
| |
| 183 | 182, 113 | brcnv 5022 |
. . . . . . . . . . . . . . . . 17
|
| 184 | 181, 183 | syl6bb 269 |
. . . . . . . . . . . . . . . 16
|
| 185 | 184 | notbid 301 |
. . . . . . . . . . . . . . 15
|
| 186 | 185 | ralbidv 2829 |
. . . . . . . . . . . . . 14
|
| 187 | 176, 177, 180, 186 | rexpr 4017 |
. . . . . . . . . . . . 13
|
| 188 | rexnal 2836 |
. . . . . . . . . . . . 13
| |
| 189 | 174, 187, 188 | 3bitr3i 283 |
. . . . . . . . . . . 12
|
| 190 | 189 | anbi2i 708 |
. . . . . . . . . . 11
|
| 191 | annim 432 |
. . . . . . . . . . 11
| |
| 192 | 190, 191 | bitri 257 |
. . . . . . . . . 10
|
| 193 | 192 | rexbii 2881 |
. . . . . . . . 9
↾t
↾t
|
| 194 | rexnal 2836 |
. . . . . . . . 9
↾t
↾t
| |
| 195 | 193, 194 | bitri 257 |
. . . . . . . 8
↾t
↾t
|
| 196 | 172, 195 | syl6ib 234 |
. . . . . . 7
↾t
|
| 197 | 196 | necon4ad 2662 |
. . . . . 6
↾t
|
| 198 | 197 | ralimdva 2805 |
. . . . 5
↾t
|
| 199 | ffn 5739 |
. . . . . 6
 | |
| 200 | 25, 199 | syl 17 |
. . . . 5
|
| 201 | 198, 200 | jctild 552 |
. . . 4
↾t
|
| 202 | fconstfv 6143 |
. . . . 5
| |
| 203 | 182 | fconst2 6137 |
. . . . 5
|
| 204 | 202, 203 | bitr3i 259 |
. . . 4
|
| 205 | 201, 204 | syl6ib 234 |
. . 3
↾t
|
| 206 | 205 | reximdva 2858 |
. 2
↾t
|
| 207 | 7, 206 | mpd 15 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 189 wo 375 wa 376 w3a 1007 wceq 1452 wcel 1904 wne 2641 wral 2756 wrex 2757 cvv 3031 wss 3390 csn 3959 cpr 3961 cuni 4190 class class class wbr 4395
cmpt 4454 cxp 4837 ccnv 4838 cdm 4839 crn 4840 cima 4842 wfun 5583 wfn 5584 wf 5585 cfv 5589 (class class class)co 6308
cmap 7490
cc 9555
cr 9556
cc0 9557
c1 9558
caddc 9560 cxr 9692 clt 9693 cle 9694 cmin 9880 cneg 9881 cn 10631 crp 11325 cioo 11660 cicc 11663 cfz 11810 cabs 13374 ↾t crest 15397 ctg 15414 cpt 15415 ctsr 16523
ctop 19994
TopOnctopon 19995 ccn 20317 ccnp 20318 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 |
| This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-disj 4367 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-omul 7205 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-acn 8394 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-sum 13830 df-dvds 14383 df-rest 15399 df-topgen 15420 df-pt 15421 df-ps 16524 df-tsr 16525 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-top 19998 df-bases 19999 df-topon 20000 df-cld 20111 df-ntr 20112 df-cls 20113 df-lp 20229 df-cn 20320 df-cnp 20321 df-t1 20407 df-haus 20408 df-cmp 20479 df-tx 20654 df-hmeo 20847 df-hmph 20848 df-ii 21987 |
| This theorem is referenced by: broucube 32038 |
| Copyright terms: Public domain | W3C validator |