![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > icossxr | Structured version Visualization version Unicode version |
Description: A closed-below, open-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.) |
Ref | Expression |
---|---|
icossxr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ico 11670 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ixxssxr 11676 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-cnex 9621 ax-resscn 9622 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-iun 4294 df-br 4417 df-opab 4476 df-mpt 4477 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-fv 5609 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-1st 6820 df-2nd 6821 df-xr 9705 df-ico 11670 |
This theorem is referenced by: leordtvallem2 20276 leordtval2 20277 nmoffn 21765 nmofval 21768 nmogelb 21770 nmolb 21771 nmof 21773 nmoffnOLD 21786 nmofvalOLD 21787 nmogelbOLD 21789 nmolbOLD 21790 nmofOLD 21791 icopnfhmeo 22020 elovolm 22477 ovolmge0 22479 ovolgelb 22482 ovollb2lem 22490 ovoliunlem1 22504 ovoliunlem2 22505 ovolscalem1 22515 ovolicc1 22518 ioombl1lem2 22561 ioombl1lem4 22563 uniioovol 22585 uniiccvol 22586 uniioombllem1 22587 uniioombllem2 22589 uniioombllem2OLD 22590 uniioombllem3 22592 uniioombllem6 22595 esumpfinvallem 28944 esummulc1 28951 esummulc2 28952 mblfinlem3 32024 mblfinlem4 32025 ismblfin 32026 itg2gt0cn 32042 xralrple2 37615 icoub 37665 elhoi 38402 hoidmvlelem5 38459 ovnhoilem1 38461 ovnhoilem2 38462 ovnhoi 38463 |
Copyright terms: Public domain | W3C validator |