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 2617 |
. . . . 5
 
  | |
| 2 | 1 | anbi1d 616 |
. . . 4
|
| 3 | opreq1 3959 |
. . . . . 6
[,) [,) | |
| 4 | 3 | uneq1d 2179 |
. . . . 5
[,) [,) [,) [,) |
| 5 | opreq1 3959 |
. . . . 5
[,) [,) | |
| 6 | 4, 5 | eqeq12d 1486 |
. . . 4
[,) [,) [,) [,) [,) [,) |
| 7 | 2, 6 | imbi12d 625 |
. . 3
[,)
[,) [,)
[,) [,)
[,) |
| 8 | breq2 2618 |
. . . . 5
| |
| 9 | breq1 2617 |
. . . . 5
| |
| 10 | 8, 9 | anbi12d 627 |
. . . 4
|
| 11 | opreq2 3960 |
. . . . . 6
[,) [,)
| |
| 12 | opreq1 3959 |
. . . . . 6
[,) [,) | |
| 13 | 11, 12 | uneq12d 2181 |
. . . . 5
[,) [,) [,)
[,) |
| 14 | 13 | eqeq1d 1480 |
. . . 4
[,) [,) [,)
[,) [,) [,) |
| 15 | 10, 14 | imbi12d 625 |
. . 3
[,) [,) [,)
[,) [,) [,) |
| 16 | breq2 2618 |
. . . . 5
| |
| 17 | 16 | anbi2d 615 |
. . . 4
|
| 18 | opreq2 3960 |
. . . . . 6
[,) [,)
| |
| 19 | 18 | uneq2d 2180 |
. . . . 5
[,)
[,)
[,) [,) |
| 20 | opreq2 3960 |
. . . . 5
[,) [,)
| |
| 21 | 19, 20 | eqeq12d 1486 |
. . . 4
[,)
[,)
[,) [,)
[,) [,) |
| 22 | 17, 21 | imbi12d 625 |
. . 3
[,) [,) [,)
[,) [,) [,) |
| 23 | 0re 5420 |
. . . . 5
| |
| 24 | 23 | elimel 2390 |
. . . 4
|
| 25 | 23 | elimel 2390 |
. . . 4
|
| 26 | 23 | elimel 2390 |
. . . 4
|
| 27 | 24, 25, 26 | icounlem 6353 |
. . 3
[,)
[,) [,) |
| 28 | 7, 15, 22, 27 | dedth3h 2384 |
. 2
[,)
[,) [,) |
| 29 | 28 | imp 350 |
1
[,) [,) [,) |
| Colors of variables: wff set class |
| Syntax hints: wi 3 wa 223 w3a 774 wceq 954 wcel 956 cun 2041 cif 2357 class class class wbr 2614
(class class class)co 3954 cr 5213 cc0 5214 cle 5275 [,)cico 6304 |
| This theorem is referenced by: efif1lem7 8670 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861 ax-inf2 4605 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-nel 1585 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2499 df-int 2529 df-iun 2563 df-br 2615 df-opab 2662 df-tr 2676 df-eprel 2827 df-id 2830 df-po 2835 df-so 2845 df-fr 2912 df-we 2929 df-ord 2946 df-on 2947 df-lim 2948 df-suc 2949 df-om 3127 df-xp 3179 df-rel 3180 df-cnv 3181 df-co |