HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The union of end-to-end closed-below, open-above real intervals. (Contributed by Paul Chapman, 15-Mar-2008.) |
| Ref | Expression |
|---|---|
| icoun |
         
 [,)  [,)  [,) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | breq1 2622 |
. . . . 5
 
  | |
| 2 | 1 | anbi1d 617 |
. . . 4
|
| 3 | opreq1 3968 |
. . . . . 6
[,) [,) | |
| 4 | 3 | uneq1d 2183 |
. . . . 5
[,) [,) [,) [,) |
| 5 | opreq1 3968 |
. . . . 5
[,) [,) | |
| 6 | 4, 5 | eqeq12d 1489 |
. . . 4
[,) [,) [,) [,) [,) [,) |
| 7 | 2, 6 | imbi12d 626 |
. . 3
[,)
[,) [,)
[,) [,)
[,) |
| 8 | breq2 2623 |
. . . . 5
| |
| 9 | breq1 2622 |
. . . . 5
| |
| 10 | 8, 9 | anbi12d 628 |
. . . 4
|
| 11 | opreq2 3969 |
. . . . . 6
[,) [,)
| |
| 12 | opreq1 3968 |
. . . . . 6
[,) [,) | |
| 13 | 11, 12 | uneq12d 2185 |
. . . . 5
[,) [,) [,)
[,) |
| 14 | 13 | eqeq1d 1483 |
. . . 4
[,) [,) [,)
[,) [,) [,) |
| 15 | 10, 14 | imbi12d 626 |
. . 3
[,) [,) [,)
[,) [,) [,) |
| 16 | breq2 2623 |
. . . . 5
| |
| 17 | 16 | anbi2d 616 |
. . . 4
|
| 18 | opreq2 3969 |
. . . . . 6
[,) [,)
| |
| 19 | 18 | uneq2d 2184 |
. . . . 5
[,)
[,)
[,) [,) |
| 20 | opreq2 3969 |
. . . . 5
[,) [,)
| |
| 21 | 19, 20 | eqeq12d 1489 |
. . . 4
[,)
[,)
[,) [,)
[,) [,) |
| 22 | 17, 21 | imbi12d 626 |
. . 3
[,) [,) [,)
[,) [,) [,) |
| 23 | 0re 5440 |
. . . . 5
| |
| 24 | 23 | elimel 2394 |
. . . 4
|
| 25 | 23 | elimel 2394 |
. . . 4
|
| 26 | 23 | elimel 2394 |
. . . 4
|
| 27 | 24, 25, 26 | icounlem 6412 |
. . 3
[,)
[,) [,) |
| 28 | 7, 15, 22, 27 | dedth3h 2388 |
. 2
[,)
[,) [,) |
| 29 | 28 | imp 350 |
1
[,) [,) [,) |
| Colors of variables: wff set class |
| Syntax hints: wi 3 wa 223 w3a 775 wceq 956 wcel 958 cun 2045 cif 2361 class class class wbr 2619
(class class class)co 3963 cr 5233 cc0 5234 cle 5295 [,)cico 6359 |
| This theorem is referenced by: efif1lem7 8736 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-9 965 ax-10 966 ax-11 967 ax-12 968 ax-13 969 ax-14 970 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-rep 2693 ax-sep 2703 ax-nul 2710 ax-pow 2742 ax-pr 2779 ax-un 2866 ax-inf2 4625 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 776 df-3an 777 df-ex 981 df-sb 1172 df-eu 1382 df-mo 1383 df-clab 1464 df-cleq 1469 df-clel 1472 df-ne 1587 df-nel 1588 df-ral 1649 df-rex 1650 df-reu 1651 df-rab 1652 df-v 1812 df-sbc 1942 df-csb 2002 df-dif 2049 df-un 2050 df-in 2051 df-ss 2053 df-pss 2055 df-nul 2281 df-if 2362 df-pw 2402 df-sn 2412 df-pr 2413 df-tp 2415 df-op 2416 df-uni 2504 df-int 2534 df-iun 2568 df-br 2620 df-opab 2667 df-tr 2681 df-eprel 2832 df-id 2835 df-po 2840 df-so 2850 df-fr 2917 df-we 2934 df-ord 2951 df-on 2952 df-lim 2953 df-suc 2954 df-om 3132 df-xp 3184 df-rel 3185 df-cnv |